elsetpreimafvssdm - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > elsetpreimafvssdm		Structured version Visualization version GIF version

Theorem elsetpreimafvssdm 46863

Description: An element of the class 𝑃 of all preimages of function values is a subset of the domain of the function. (Contributed by AV, 8-Mar-2024.)

**Hypothesis**
Ref	Expression
setpreimafvex.p	⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (^◡𝐹 “ {(𝐹‘𝑥)})}

**Assertion**
Ref	Expression
elsetpreimafvssdm	⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃) → 𝑆 ⊆ 𝐴)

Distinct variable groups: 𝑥,𝐴,𝑧 𝑥,𝐹,𝑧 𝑥,𝑆,𝑧 Allowed substitution hints: 𝑃(𝑥,𝑧)

**Proof of Theorem elsetpreimafvssdm**
Step	Hyp	Ref	Expression
1		setpreimafvex.p	. . . 4 ⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (^◡𝐹 “ {(𝐹‘𝑥)})}
2	1	elsetpreimafv 46862	. . 3 ⊢ (𝑆 ∈ 𝑃 → ∃𝑥 ∈ 𝐴 𝑆 = (^◡𝐹 “ {(𝐹‘𝑥)}))
3		cnvimass 6086	. . . . . . . . 9 ⊢ (^◡𝐹 “ {(𝐹‘𝑥)}) ⊆ dom 𝐹
4		fndm 6658	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	3, 4	sseqtrid 4029	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (^◡𝐹 “ {(𝐹‘𝑥)}) ⊆ 𝐴)
6	5	adantr 479	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (^◡𝐹 “ {(𝐹‘𝑥)}) ⊆ 𝐴)
7		sseq1 4002	. . . . . . 7 ⊢ (𝑆 = (^◡𝐹 “ {(𝐹‘𝑥)}) → (𝑆 ⊆ 𝐴 ↔ (^◡𝐹 “ {(𝐹‘𝑥)}) ⊆ 𝐴))
8	6, 7	syl5ibrcom 246	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑆 = (^◡𝐹 “ {(𝐹‘𝑥)}) → 𝑆 ⊆ 𝐴))
9	8	expcom 412	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝑆 = (^◡𝐹 “ {(𝐹‘𝑥)}) → 𝑆 ⊆ 𝐴)))
10	9	com23 86	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (𝑆 = (^◡𝐹 “ {(𝐹‘𝑥)}) → (𝐹 Fn 𝐴 → 𝑆 ⊆ 𝐴)))
11	10	rexlimiv 3137	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑆 = (^◡𝐹 “ {(𝐹‘𝑥)}) → (𝐹 Fn 𝐴 → 𝑆 ⊆ 𝐴))
12	2, 11	syl 17	. 2 ⊢ (𝑆 ∈ 𝑃 → (𝐹 Fn 𝐴 → 𝑆 ⊆ 𝐴))
13	12	impcom 406	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃) → 𝑆 ⊆ 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 {cab 2702 ∃wrex 3059 ⊆ wss 3944 {csn 4630 ^◡ccnv 5677 dom cdm 5678 “ cima 5681 Fn wfn 6544 ‘cfv 6549

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-xp 5684 df-cnv 5686 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-fn 6552

This theorem is referenced by: preimafvsspwdm 46866 uniimaelsetpreimafv 46873

W3C validator

	
		OSZAR »