fnpreimac

Description: Choose a set x containing a preimage of each element of a given set B . (Contributed by Thierry Arnoux, 7-May-2023)

		Ref	Expression
	Assertion	fnpreimac	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to \exists x \in 𝒫 A (x \approx B \land F [x] = B)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (y \in B ⟼ F^{-1} [\{y\}]) = (y \in B ⟼ F^{-1} [\{y\}])$
2	1	elrnmpt	$⊢ z \in V \to (z \in ran (y \in B ⟼ F^{-1} [\{y\}]) \leftrightarrow \exists y \in B z = F^{-1} [\{y\}])$
3	2	elv	$⊢ z \in ran (y \in B ⟼ F^{-1} [\{y\}]) \leftrightarrow \exists y \in B z = F^{-1} [\{y\}]$
4		simpr	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \land z = F^{-1} [\{y\}]) \to z = F^{-1} [\{y\}]$
5		simpl3	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to B \subseteq ran F$
6		simpr	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to y \in B$
7	5 6	sseldd	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to y \in ran F$
8		inisegn0	$⊢ y \in ran F \leftrightarrow F^{-1} [\{y\}] \neq \emptyset$
9	7 8	sylib	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to F^{-1} [\{y\}] \neq \emptyset$
10	9	adantr	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \land z = F^{-1} [\{y\}]) \to F^{-1} [\{y\}] \neq \emptyset$
11	4 10	eqnetrd	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \land z = F^{-1} [\{y\}]) \to z \neq \emptyset$
12	11	r19.29an	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land \exists y \in B z = F^{-1} [\{y\}]) \to z \neq \emptyset$
13	3 12	sylan2b	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land z \in ran (y \in B ⟼ F^{-1} [\{y\}])) \to z \neq \emptyset$
14	13	ralrimiva	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) z \neq \emptyset$
15		simp2	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to F Fn A$
16		simp1	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to A \in V$
17	15 16	jca	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to (F Fn A \land A \in V)$
18		fnex	$⊢ (F Fn A \land A \in V) \to F \in V$
19		rnexg	$⊢ F \in V \to ran F \in V$
20	17 18 19	3syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ran F \in V$
21		simp3	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to B \subseteq ran F$
22	20 21	ssexd	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to B \in V$
23		mptexg	$⊢ B \in V \to (y \in B ⟼ F^{-1} [\{y\}]) \in V$
24		rnexg	$⊢ (y \in B ⟼ F^{-1} [\{y\}]) \in V \to ran (y \in B ⟼ F^{-1} [\{y\}]) \in V$
25		fvi	$⊢ ran (y \in B ⟼ F^{-1} [\{y\}]) \in V \to I (ran (y \in B ⟼ F^{-1} [\{y\}])) = ran (y \in B ⟼ F^{-1} [\{y\}])$
26	22 23 24 25	4syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to I (ran (y \in B ⟼ F^{-1} [\{y\}])) = ran (y \in B ⟼ F^{-1} [\{y\}])$
27	14 26	raleqtrrdv	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to \forall z \in I (ran (y \in B ⟼ F^{-1} [\{y\}])) z \neq \emptyset$
28		fvex	$⊢ I (ran (y \in B ⟼ F^{-1} [\{y\}])) \in V$
29	28	ac5b	$⊢ \forall z \in I (ran (y \in B ⟼ F^{-1} [\{y\}])) z \neq \emptyset \to \exists f (f : I (ran (y \in B ⟼ F^{-1} [\{y\}])) ⟶ ⋃ I (ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in I (ran (y \in B ⟼ F^{-1} [\{y\}])) f (z) \in z)$
30	27 29	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to \exists f (f : I (ran (y \in B ⟼ F^{-1} [\{y\}])) ⟶ ⋃ I (ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in I (ran (y \in B ⟼ F^{-1} [\{y\}])) f (z) \in z)$
31	26	unieqd	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ⋃ I (ran (y \in B ⟼ F^{-1} [\{y\}])) = ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
32	26 31	feq23d	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to (f : I (ran (y \in B ⟼ F^{-1} [\{y\}])) ⟶ ⋃ I (ran (y \in B ⟼ F^{-1} [\{y\}])) \leftrightarrow f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]))$
33	26	raleqdv	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to (\forall z \in I (ran (y \in B ⟼ F^{-1} [\{y\}])) f (z) \in z \leftrightarrow \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z)$
34	32 33	anbi12d	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ((f : I (ran (y \in B ⟼ F^{-1} [\{y\}])) ⟶ ⋃ I (ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in I (ran (y \in B ⟼ F^{-1} [\{y\}])) f (z) \in z) \leftrightarrow (f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z))$
35	34	exbidv	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to (\exists f (f : I (ran (y \in B ⟼ F^{-1} [\{y\}])) ⟶ ⋃ I (ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in I (ran (y \in B ⟼ F^{-1} [\{y\}])) f (z) \in z) \leftrightarrow \exists f (f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z))$
36	30 35	mpbid	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to \exists f (f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z)$
37		vex	$⊢ f \in V$
38	37	rnex	$⊢ ran f \in V$
39	38	a1i	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ran f \in V$
40		simplr	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
41		frn	$⊢ f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \to ran f \subseteq ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
42	40 41	syl	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ran f \subseteq ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
43		nfv	$⊢ Ⅎ y (A \in V \land F Fn A \land B \subseteq ran F)$
44		nfcv	$⊢ \underline{Ⅎ} y f$
45		nfmpt1	$⊢ \underline{Ⅎ} y (y \in B ⟼ F^{-1} [\{y\}])$
46	45	nfrn	$⊢ \underline{Ⅎ} y ran (y \in B ⟼ F^{-1} [\{y\}])$
47	46	nfuni	$⊢ \underline{Ⅎ} y ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
48	44 46 47	nff	$⊢ Ⅎ y f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
49	43 48	nfan	$⊢ Ⅎ y ((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]))$
50		nfv	$⊢ Ⅎ y f (z) \in z$
51	46 50	nfralw	$⊢ Ⅎ y \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z$
52	49 51	nfan	$⊢ Ⅎ y (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z)$
53	17 18	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to F \in V$
54	53	ad3antrrr	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \to F \in V$
55		cnvexg	$⊢ F \in V \to F^{-1} \in V$
56		imaexg	$⊢ F^{-1} \in V \to F^{-1} [\{y\}] \in V$
57	54 55 56	3syl	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \to F^{-1} [\{y\}] \in V$
58		cnvimass	$⊢ F^{-1} [\{y\}] \subseteq dom F$
59	58	a1i	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \to F^{-1} [\{y\}] \subseteq dom F$
60	15	fndmd	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to dom F = A$
61	60	ad3antrrr	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \to dom F = A$
62	59 61	sseqtrd	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \to F^{-1} [\{y\}] \subseteq A$
63	57 62	elpwd	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \to F^{-1} [\{y\}] \in 𝒫 A$
64	63	ex	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (y \in B \to F^{-1} [\{y\}] \in 𝒫 A)$
65	52 64	ralrimi	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to \forall y \in B F^{-1} [\{y\}] \in 𝒫 A$
66	1	rnmptss	$⊢ \forall y \in B F^{-1} [\{y\}] \in 𝒫 A \to ran (y \in B ⟼ F^{-1} [\{y\}]) \subseteq 𝒫 A$
67	65 66	syl	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ran (y \in B ⟼ F^{-1} [\{y\}]) \subseteq 𝒫 A$
68		sspwuni	$⊢ ran (y \in B ⟼ F^{-1} [\{y\}]) \subseteq 𝒫 A \leftrightarrow ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \subseteq A$
69	67 68	sylib	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \subseteq A$
70	42 69	sstrd	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ran f \subseteq A$
71	39 70	elpwd	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ran f \in 𝒫 A$
72		fnfun	$⊢ F Fn A \to Fun F$
73	15 72	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to Fun F$
74	73	ad5antr	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to Fun F$
75		sndisj	$⊢ \underset{y \in B}{Disj} \{y\}$
76		disjpreima	$⊢ (Fun F \land \underset{y \in B}{Disj} \{y\}) \to \underset{y \in B}{Disj} F^{-1} [\{y\}]$
77	74 75 76	sylancl	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to \underset{y \in B}{Disj} F^{-1} [\{y\}]$
78		disjrnmpt	$⊢ \underset{y \in B}{Disj} F^{-1} [\{y\}] \to \underset{z \in ran (y \in B ⟼ F^{-1} [\{y\}])}{Disj} z$
79	77 78	syl	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to \underset{z \in ran (y \in B ⟼ F^{-1} [\{y\}])}{Disj} z$
80		simpllr	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to u \in ran (y \in B ⟼ F^{-1} [\{y\}])$
81		simplr	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to v \in ran (y \in B ⟼ F^{-1} [\{y\}])$
82		simp-4r	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z$
83		fveq2	$⊢ z = u \to f (z) = f (u)$
84		id	$⊢ z = u \to z = u$
85	83 84	eleq12d	$⊢ z = u \to (f (z) \in z \leftrightarrow f (u) \in u)$
86	85	rspcv	$⊢ u \in ran (y \in B ⟼ F^{-1} [\{y\}]) \to (\forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z \to f (u) \in u)$
87	86	imp	$⊢ (u \in ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to f (u) \in u$
88	80 82 87	syl2anc	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to f (u) \in u$
89		simpr	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to f (u) = f (v)$
90		fveq2	$⊢ z = v \to f (z) = f (v)$
91		id	$⊢ z = v \to z = v$
92	90 91	eleq12d	$⊢ z = v \to (f (z) \in z \leftrightarrow f (v) \in v)$
93	92	rspcv	$⊢ v \in ran (y \in B ⟼ F^{-1} [\{y\}]) \to (\forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z \to f (v) \in v)$
94	93	imp	$⊢ (v \in ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to f (v) \in v$
95	81 82 94	syl2anc	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to f (v) \in v$
96	89 95	eqeltrd	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to f (u) \in v$
97	84 91	disji	$⊢ (\underset{z \in ran (y \in B ⟼ F^{-1} [\{y\}])}{Disj} z \land (u \in ran (y \in B ⟼ F^{-1} [\{y\}]) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land (f (u) \in u \land f (u) \in v)) \to u = v$
98	79 80 81 88 96 97	syl122anc	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land f (u) = f (v)) \to u = v$
99	98	ex	$⊢ (((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land u \in ran (y \in B ⟼ F^{-1} [\{y\}])) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}])) \to (f (u) = f (v) \to u = v)$
100	99	anasss	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land (u \in ran (y \in B ⟼ F^{-1} [\{y\}]) \land v \in ran (y \in B ⟼ F^{-1} [\{y\}]))) \to (f (u) = f (v) \to u = v)$
101	100	ralrimivva	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to \forall u \in ran (y \in B ⟼ F^{-1} [\{y\}]) \forall v \in ran (y \in B ⟼ F^{-1} [\{y\}]) (f (u) = f (v) \to u = v)$
102	40 101	jca	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall u \in ran (y \in B ⟼ F^{-1} [\{y\}]) \forall v \in ran (y \in B ⟼ F^{-1} [\{y\}]) (f (u) = f (v) \to u = v))$
103		dff13	$⊢ f : ran (y \in B ⟼ F^{-1} [\{y\}]) \underset{1-1}{⟶} ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \leftrightarrow (f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall u \in ran (y \in B ⟼ F^{-1} [\{y\}]) \forall v \in ran (y \in B ⟼ F^{-1} [\{y\}]) (f (u) = f (v) \to u = v))$
104	102 103	sylibr	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to f : ran (y \in B ⟼ F^{-1} [\{y\}]) \underset{1-1}{⟶} ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
105		f1f1orn	$⊢ f : ran (y \in B ⟼ F^{-1} [\{y\}]) \underset{1-1}{⟶} ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \to f : ran (y \in B ⟼ F^{-1} [\{y\}]) \underset{1-1 onto}{⟶} ran f$
106	104 105	syl	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to f : ran (y \in B ⟼ F^{-1} [\{y\}]) \underset{1-1 onto}{⟶} ran f$
107		f1oen3g	$⊢ (f \in V \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) \underset{1-1 onto}{⟶} ran f) \to ran (y \in B ⟼ F^{-1} [\{y\}]) \approx ran f$
108	37 106 107	sylancr	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ran (y \in B ⟼ F^{-1} [\{y\}]) \approx ran f$
109	108	ensymd	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ran f \approx ran (y \in B ⟼ F^{-1} [\{y\}])$
110	22 23	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to (y \in B ⟼ F^{-1} [\{y\}]) \in V$
111	110	ad2antrr	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (y \in B ⟼ F^{-1} [\{y\}]) \in V$
112	57	ex	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (y \in B \to F^{-1} [\{y\}] \in V)$
113	52 112	ralrimi	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to \forall y \in B F^{-1} [\{y\}] \in V$
114	73	ad5antr	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \land y \neq t) \to Fun F$
115		simpr	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \land y \neq t) \to y \neq t$
116	21	ad5antr	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \land y \neq t) \to B \subseteq ran F$
117		simpllr	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \land y \neq t) \to y \in B$
118	116 117	sseldd	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \land y \neq t) \to y \in ran F$
119		simplr	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \land y \neq t) \to t \in B$
120	116 119	sseldd	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \land y \neq t) \to t \in ran F$
121	114 115 118 120	preimane	$⊢ ((((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \land y \neq t) \to F^{-1} [\{y\}] \neq F^{-1} [\{t\}]$
122	121	ex	$⊢ (((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \to (y \neq t \to F^{-1} [\{y\}] \neq F^{-1} [\{t\}])$
123	122	necon4d	$⊢ (((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \land t \in B) \to (F^{-1} [\{y\}] = F^{-1} [\{t\}] \to y = t)$
124	123	ralrimiva	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land y \in B) \to \forall t \in B (F^{-1} [\{y\}] = F^{-1} [\{t\}] \to y = t)$
125	124	ex	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (y \in B \to \forall t \in B (F^{-1} [\{y\}] = F^{-1} [\{t\}] \to y = t))$
126	52 125	ralrimi	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to \forall y \in B \forall t \in B (F^{-1} [\{y\}] = F^{-1} [\{t\}] \to y = t)$
127	113 126	jca	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (\forall y \in B F^{-1} [\{y\}] \in V \land \forall y \in B \forall t \in B (F^{-1} [\{y\}] = F^{-1} [\{t\}] \to y = t))$
128		sneq	$⊢ y = t \to \{y\} = \{t\}$
129	128	imaeq2d	$⊢ y = t \to F^{-1} [\{y\}] = F^{-1} [\{t\}]$
130	1 129	f1mpt	$⊢ (y \in B ⟼ F^{-1} [\{y\}]) : B \underset{1-1}{⟶} V \leftrightarrow (\forall y \in B F^{-1} [\{y\}] \in V \land \forall y \in B \forall t \in B (F^{-1} [\{y\}] = F^{-1} [\{t\}] \to y = t))$
131	127 130	sylibr	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (y \in B ⟼ F^{-1} [\{y\}]) : B \underset{1-1}{⟶} V$
132		f1f1orn	$⊢ (y \in B ⟼ F^{-1} [\{y\}]) : B \underset{1-1}{⟶} V \to (y \in B ⟼ F^{-1} [\{y\}]) : B \underset{1-1 onto}{⟶} ran (y \in B ⟼ F^{-1} [\{y\}])$
133	131 132	syl	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (y \in B ⟼ F^{-1} [\{y\}]) : B \underset{1-1 onto}{⟶} ran (y \in B ⟼ F^{-1} [\{y\}])$
134		f1oen3g	$⊢ ((y \in B ⟼ F^{-1} [\{y\}]) \in V \land (y \in B ⟼ F^{-1} [\{y\}]) : B \underset{1-1 onto}{⟶} ran (y \in B ⟼ F^{-1} [\{y\}])) \to B \approx ran (y \in B ⟼ F^{-1} [\{y\}])$
135	111 133 134	syl2anc	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to B \approx ran (y \in B ⟼ F^{-1} [\{y\}])$
136	135	ensymd	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ran (y \in B ⟼ F^{-1} [\{y\}]) \approx B$
137		entr	$⊢ (ran f \approx ran (y \in B ⟼ F^{-1} [\{y\}]) \land ran (y \in B ⟼ F^{-1} [\{y\}]) \approx B) \to ran f \approx B$
138	109 136 137	syl2anc	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ran f \approx B$
139		imass2	$⊢ ran f \subseteq ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \to F [ran f] \subseteq F [⋃ ran (y \in B ⟼ F^{-1} [\{y\}])]$
140	41 139	syl	$⊢ f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \to F [ran f] \subseteq F [⋃ ran (y \in B ⟼ F^{-1} [\{y\}])]$
141	40 140	syl	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to F [ran f] \subseteq F [⋃ ran (y \in B ⟼ F^{-1} [\{y\}])]$
142		imauni	$⊢ F [⋃ ran (y \in B ⟼ F^{-1} [\{y\}])] = ⋃_{z \in ran (y \in B ⟼ F^{-1} [\{y\}])} F [z]$
143		imaeq2	$⊢ z = F^{-1} [\{y\}] \to F [z] = F [F^{-1} [\{y\}]]$
144	53	adantr	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to F \in V$
145	144 55 56	3syl	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to F^{-1} [\{y\}] \in V$
146	143 145	iunrnmptss	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ⋃_{z \in ran (y \in B ⟼ F^{-1} [\{y\}])} F [z] \subseteq ⋃_{y \in B} F [F^{-1} [\{y\}]]$
147		funimacnv	$⊢ Fun F \to F [F^{-1} [\{y\}]] = \{y\} \cap ran F$
148	73 147	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to F [F^{-1} [\{y\}]] = \{y\} \cap ran F$
149	148	adantr	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to F [F^{-1} [\{y\}]] = \{y\} \cap ran F$
150	6	snssd	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to \{y\} \subseteq B$
151	150 5	sstrd	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to \{y\} \subseteq ran F$
152		dfss2	$⊢ \{y\} \subseteq ran F \leftrightarrow \{y\} \cap ran F = \{y\}$
153	151 152	sylib	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to \{y\} \cap ran F = \{y\}$
154	149 153	eqtrd	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to F [F^{-1} [\{y\}]] = \{y\}$
155	154	iuneq2dv	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ⋃_{y \in B} F [F^{-1} [\{y\}]] = ⋃_{y \in B} \{y\}$
156		iunid	$⊢ ⋃_{y \in B} \{y\} = B$
157	155 156	eqtrdi	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ⋃_{y \in B} F [F^{-1} [\{y\}]] = B$
158	146 157	sseqtrd	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ⋃_{z \in ran (y \in B ⟼ F^{-1} [\{y\}])} F [z] \subseteq B$
159	158	ad2antrr	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to ⋃_{z \in ran (y \in B ⟼ F^{-1} [\{y\}])} F [z] \subseteq B$
160	142 159	eqsstrid	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to F [⋃ ran (y \in B ⟼ F^{-1} [\{y\}])] \subseteq B$
161	141 160	sstrd	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to F [ran f] \subseteq B$
162	40	adantr	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
163	162	ffund	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to Fun f$
164		simpr	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to t \in B$
165	53 55	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to F^{-1} \in V$
166	165	ad3antrrr	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to F^{-1} \in V$
167		imaexg	$⊢ F^{-1} \in V \to F^{-1} [\{t\}] \in V$
168	166 167	syl	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to F^{-1} [\{t\}] \in V$
169	1 129	elrnmpt1s	$⊢ (t \in B \land F^{-1} [\{t\}] \in V) \to F^{-1} [\{t\}] \in ran (y \in B ⟼ F^{-1} [\{y\}])$
170	164 168 169	syl2anc	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to F^{-1} [\{t\}] \in ran (y \in B ⟼ F^{-1} [\{y\}])$
171	162	fdmd	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to dom f = ran (y \in B ⟼ F^{-1} [\{y\}])$
172	170 171	eleqtrrd	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to F^{-1} [\{t\}] \in dom f$
173		fvelrn	$⊢ (Fun f \land F^{-1} [\{t\}] \in dom f) \to f (F^{-1} [\{t\}]) \in ran f$
174	163 172 173	syl2anc	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to f (F^{-1} [\{t\}]) \in ran f$
175	15	ad3antrrr	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to F Fn A$
176		simplr	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z$
177		fveq2	$⊢ z = F^{-1} [\{t\}] \to f (z) = f (F^{-1} [\{t\}])$
178		id	$⊢ z = F^{-1} [\{t\}] \to z = F^{-1} [\{t\}]$
179	177 178	eleq12d	$⊢ z = F^{-1} [\{t\}] \to (f (z) \in z \leftrightarrow f (F^{-1} [\{t\}]) \in F^{-1} [\{t\}])$
180	179	rspcv	$⊢ F^{-1} [\{t\}] \in ran (y \in B ⟼ F^{-1} [\{y\}]) \to (\forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z \to f (F^{-1} [\{t\}]) \in F^{-1} [\{t\}])$
181	180	imp	$⊢ (F^{-1} [\{t\}] \in ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to f (F^{-1} [\{t\}]) \in F^{-1} [\{t\}]$
182	170 176 181	syl2anc	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to f (F^{-1} [\{t\}]) \in F^{-1} [\{t\}]$
183		fniniseg	$⊢ F Fn A \to (f (F^{-1} [\{t\}]) \in F^{-1} [\{t\}] \leftrightarrow (f (F^{-1} [\{t\}]) \in A \land F (f (F^{-1} [\{t\}])) = t))$
184	183	simplbda	$⊢ (F Fn A \land f (F^{-1} [\{t\}]) \in F^{-1} [\{t\}]) \to F (f (F^{-1} [\{t\}])) = t$
185	175 182 184	syl2anc	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to F (f (F^{-1} [\{t\}])) = t$
186		fveqeq2	$⊢ k = f (F^{-1} [\{t\}]) \to (F (k) = t \leftrightarrow F (f (F^{-1} [\{t\}])) = t)$
187	186	rspcev	$⊢ (f (F^{-1} [\{t\}]) \in ran f \land F (f (F^{-1} [\{t\}])) = t) \to \exists k \in ran f F (k) = t$
188	174 185 187	syl2anc	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to \exists k \in ran f F (k) = t$
189	70	adantr	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to ran f \subseteq A$
190	175 189	fvelimabd	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to (t \in F [ran f] \leftrightarrow \exists k \in ran f F (k) = t)$
191	188 190	mpbird	$⊢ ((((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \land t \in B) \to t \in F [ran f]$
192	191	ex	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (t \in B \to t \in F [ran f])$
193	192	ssrdv	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to B \subseteq F [ran f]$
194	161 193	eqssd	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to F [ran f] = B$
195	138 194	jca	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to (ran f \approx B \land F [ran f] = B)$
196		breq1	$⊢ x = ran f \to (x \approx B \leftrightarrow ran f \approx B)$
197		imaeq2	$⊢ x = ran f \to F [x] = F [ran f]$
198	197	eqeq1d	$⊢ x = ran f \to (F [x] = B \leftrightarrow F [ran f] = B)$
199	196 198	anbi12d	$⊢ x = ran f \to ((x \approx B \land F [x] = B) \leftrightarrow (ran f \approx B \land F [ran f] = B))$
200	199	rspcev	$⊢ (ran f \in 𝒫 A \land (ran f \approx B \land F [ran f] = B)) \to \exists x \in 𝒫 A (x \approx B \land F [x] = B)$
201	71 195 200	syl2anc	$⊢ (((A \in V \land F Fn A \land B \subseteq ran F) \land f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to \exists x \in 𝒫 A (x \approx B \land F [x] = B)$
202	201	anasss	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land (f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z)) \to \exists x \in 𝒫 A (x \approx B \land F [x] = B)$
203	202	ex	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ((f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to \exists x \in 𝒫 A (x \approx B \land F [x] = B))$
204	203	exlimdv	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to (\exists f (f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \land \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z) \to \exists x \in 𝒫 A (x \approx B \land F [x] = B))$
205	36 204	mpd	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to \exists x \in 𝒫 A (x \approx B \land F [x] = B)$

Metamath Proof Explorer

Theorem fnpreimac

Proof