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	22 23 24	3syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ran (y \in B ⟼ F^{-1} [\{y\}]) \in V$
26		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\}])$
27	25 26	syl	$⊢ (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\}])$
28	27	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\}])) z \neq \emptyset \leftrightarrow \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) z \neq \emptyset)$
29	14 28	mpbird	$⊢ (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$
30		fvex	$⊢ I (ran (y \in B ⟼ F^{-1} [\{y\}])) \in V$
31	30	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)$
32	29 31	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)$
33	27	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\}])$
34	27 33	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\}]))$
35	27	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)$
36	34 35	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))$
37	36	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))$
38	32 37	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)$
39		vex	$⊢ f \in V$
40	39	rnex	$⊢ ran f \in V$
41	40	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$
42		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\}])$
43		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\}])$
44	42 43	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\}])$
45		nfv	$⊢ Ⅎ y (A \in V \land F Fn A \land B \subseteq ran F)$
46		nfcv	$⊢ \underline{Ⅎ} y f$
47		nfmpt1	$⊢ \underline{Ⅎ} y (y \in B ⟼ F^{-1} [\{y\}])$
48	47	nfrn	$⊢ \underline{Ⅎ} y ran (y \in B ⟼ F^{-1} [\{y\}])$
49	48	nfuni	$⊢ \underline{Ⅎ} y ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
50	46 48 49	nff	$⊢ Ⅎ y f : ran (y \in B ⟼ F^{-1} [\{y\}]) ⟶ ⋃ ran (y \in B ⟼ F^{-1} [\{y\}])$
51	45 50	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\}]))$
52		nfv	$⊢ Ⅎ y f (z) \in z$
53	48 52	nfralw	$⊢ Ⅎ y \forall z \in ran (y \in B ⟼ F^{-1} [\{y\}]) f (z) \in z$
54	51 53	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)$
55	17 18	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to F \in V$
56	55	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$
57		cnvexg	$⊢ F \in V \to F^{-1} \in V$
58		imaexg	$⊢ F^{-1} \in V \to F^{-1} [\{y\}] \in V$
59	56 57 58	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$
60		cnvimass	$⊢ F^{-1} [\{y\}] \subseteq dom F$
61	60	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$
62	15	fndmd	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to dom F = A$
63	62	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$
64	61 63	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$
65	59 64	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$
66	65	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)$
67	54 66	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$
68	1	rnmptss	$⊢ \forall y \in B F^{-1} [\{y\}] \in 𝒫 A \to ran (y \in B ⟼ F^{-1} [\{y\}]) \subseteq 𝒫 A$
69	67 68	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$
70		sspwuni	$⊢ ran (y \in B ⟼ F^{-1} [\{y\}]) \subseteq 𝒫 A \leftrightarrow ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \subseteq A$
71	69 70	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$
72	44 71	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$
73	41 72	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$
74		fnfun	$⊢ F Fn A \to Fun F$
75	15 74	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to Fun F$
76	75	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$
77		sndisj	$⊢ \underset{y \in B}{Disj} \{y\}$
78		disjpreima	$⊢ (Fun F \land \underset{y \in B}{Disj} \{y\}) \to \underset{y \in B}{Disj} F^{-1} [\{y\}]$
79	76 77 78	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\}]$
80		disjrnmpt	$⊢ \underset{y \in B}{Disj} F^{-1} [\{y\}] \to \underset{z \in ran (y \in B ⟼ F^{-1} [\{y\}])}{Disj} z$
81	79 80	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$
82		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\}])$
83		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\}])$
84		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$
85		fveq2	$⊢ z = u \to f (z) = f (u)$
86		id	$⊢ z = u \to z = u$
87	85 86	eleq12d	$⊢ z = u \to (f (z) \in z \leftrightarrow f (u) \in u)$
88	87	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)$
89	88	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$
90	82 84 89	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$
91		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)$
92		fveq2	$⊢ z = v \to f (z) = f (v)$
93		id	$⊢ z = v \to z = v$
94	92 93	eleq12d	$⊢ z = v \to (f (z) \in z \leftrightarrow f (v) \in v)$
95	94	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)$
96	95	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$
97	83 84 96	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$
98	91 97	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$
99	86 93	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$
100	81 82 83 90 98 99	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$
101	100	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)$
102	101	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)$
103	102	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)$
104	42 103	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))$
105		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))$
106	104 105	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\}])$
107		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$
108	106 107	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$
109		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$
110	39 108 109	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$
111	110	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\}])$
112	22 23	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to (y \in B ⟼ F^{-1} [\{y\}]) \in V$
113	112	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$
114	59	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)$
115	54 114	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$
116	75	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$
117		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$
118	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$
119		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$
120	118 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 y \in ran F$
121		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$
122	118 121	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$
123	116 117 120 122	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\}]$
124	123	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\}])$
125	124	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)$
126	125	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)$
127	126	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))$
128	54 127	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)$
129	115 128	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))$
130		sneq	$⊢ y = t \to \{y\} = \{t\}$
131	130	imaeq2d	$⊢ y = t \to F^{-1} [\{y\}] = F^{-1} [\{t\}]$
132	1 131	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))$
133	129 132	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$
134		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\}])$
135	133 134	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\}])$
136		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\}])$
137	113 135 136	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\}])$
138	137	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$
139		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$
140	111 138 139	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$
141		imass2	$⊢ ran f \subseteq ⋃ ran (y \in B ⟼ F^{-1} [\{y\}]) \to F [ran f] \subseteq F [⋃ ran (y \in B ⟼ F^{-1} [\{y\}])]$
142	43 141	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\}])]$
143	42 142	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\}])]$
144		imauni	$⊢ F [⋃ ran (y \in B ⟼ F^{-1} [\{y\}])] = ⋃_{z \in ran (y \in B ⟼ F^{-1} [\{y\}])} F [z]$
145		imaeq2	$⊢ z = F^{-1} [\{y\}] \to F [z] = F [F^{-1} [\{y\}]]$
146	55	adantr	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to F \in V$
147	146 57 58	3syl	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to F^{-1} [\{y\}] \in V$
148	145 147	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\}]]$
149		funimacnv	$⊢ Fun F \to F [F^{-1} [\{y\}]] = \{y\} \cap ran F$
150	75 149	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to F [F^{-1} [\{y\}]] = \{y\} \cap ran F$
151	150	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$
152	6	snssd	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to \{y\} \subseteq B$
153	152 5	sstrd	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to \{y\} \subseteq ran F$
154		df-ss	$⊢ \{y\} \subseteq ran F \leftrightarrow \{y\} \cap ran F = \{y\}$
155	153 154	sylib	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to \{y\} \cap ran F = \{y\}$
156	151 155	eqtrd	$⊢ ((A \in V \land F Fn A \land B \subseteq ran F) \land y \in B) \to F [F^{-1} [\{y\}]] = \{y\}$
157	156	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\}$
158		iunid	$⊢ ⋃_{y \in B} \{y\} = B$
159	157 158	eqtrdi	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to ⋃_{y \in B} F [F^{-1} [\{y\}]] = B$
160	148 159	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$
161	160	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$
162	144 161	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$
163	143 162	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$
164	42	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\}])$
165	164	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$
166		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$
167	55 57	syl	$⊢ (A \in V \land F Fn A \land B \subseteq ran F) \to F^{-1} \in V$
168	167	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$
169		imaexg	$⊢ F^{-1} \in V \to F^{-1} [\{t\}] \in V$
170	168 169	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$
171	1 131	elrnmpt1s	$⊢ (t \in B \land F^{-1} [\{t\}] \in V) \to F^{-1} [\{t\}] \in ran (y \in B ⟼ F^{-1} [\{y\}])$
172	166 170 171	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\}])$
173	164	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\}])$
174	172 173	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$
175		fvelrn	$⊢ (Fun f \land F^{-1} [\{t\}] \in dom f) \to f (F^{-1} [\{t\}]) \in ran f$
176	165 174 175	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$
177	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$
178		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$
179		fveq2	$⊢ z = F^{-1} [\{t\}] \to f (z) = f (F^{-1} [\{t\}])$
180		id	$⊢ z = F^{-1} [\{t\}] \to z = F^{-1} [\{t\}]$
181	179 180	eleq12d	$⊢ z = F^{-1} [\{t\}] \to (f (z) \in z \leftrightarrow f (F^{-1} [\{t\}]) \in F^{-1} [\{t\}])$
182	181	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\}])$
183	182	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\}]$
184	172 178 183	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\}]$
185		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))$
186	185	simplbda	$⊢ (F Fn A \land f (F^{-1} [\{t\}]) \in F^{-1} [\{t\}]) \to F (f (F^{-1} [\{t\}])) = t$
187	177 184 186	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$
188		fveqeq2	$⊢ k = f (F^{-1} [\{t\}]) \to (F (k) = t \leftrightarrow F (f (F^{-1} [\{t\}])) = t)$
189	188	rspcev	$⊢ (f (F^{-1} [\{t\}]) \in ran f \land F (f (F^{-1} [\{t\}])) = t) \to \exists k \in ran f F (k) = t$
190	176 187 189	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$
191	72	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$
192	177 191	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)$
193	190 192	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]$
194	193	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])$
195	194	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]$
196	163 195	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$
197	140 196	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)$
198		breq1	$⊢ x = ran f \to (x \approx B \leftrightarrow ran f \approx B)$
199		imaeq2	$⊢ x = ran f \to F [x] = F [ran f]$
200	199	eqeq1d	$⊢ x = ran f \to (F [x] = B \leftrightarrow F [ran f] = B)$
201	198 200	anbi12d	$⊢ x = ran f \to ((x \approx B \land F [x] = B) \leftrightarrow (ran f \approx B \land F [ran f] = B))$
202	201	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)$
203	73 197 202	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)$
204	203	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)$
205	204	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))$
206	205	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))$
207	38 206	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