locfinreflem

Description: A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf , it is expressed by exposing a function f from the original cover U , which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020)

	Ref	Expression
Hypotheses	locfinref.x	$⊢ X = ⋃ J$
	locfinref.1	$⊢ φ \to U \subseteq J$
	locfinref.2	$⊢ φ \to X = ⋃ U$
	locfinref.3	$⊢ φ \to V \subseteq J$
	locfinref.4	$⊢ φ \to V Ref U$
	locfinref.5	$⊢ φ \to V \in LocFin (J)$
Assertion	locfinreflem	$⊢ φ \to \exists f ((Fun f \land dom f \subseteq U \land ran f \subseteq J) \land (ran f Ref U \land ran f \in LocFin (J)))$

Proof

Step	Hyp	Ref	Expression
1		locfinref.x	$⊢ X = ⋃ J$
2		locfinref.1	$⊢ φ \to U \subseteq J$
3		locfinref.2	$⊢ φ \to X = ⋃ U$
4		locfinref.3	$⊢ φ \to V \subseteq J$
5		locfinref.4	$⊢ φ \to V Ref U$
6		locfinref.5	$⊢ φ \to V \in LocFin (J)$
7		reff	$⊢ V \in LocFin (J) \to (V Ref U \leftrightarrow (⋃ U \subseteq ⋃ V \land \exists g (g : V ⟶ U \land \forall v \in V v \subseteq g (v))))$
8	6 7	syl	$⊢ φ \to (V Ref U \leftrightarrow (⋃ U \subseteq ⋃ V \land \exists g (g : V ⟶ U \land \forall v \in V v \subseteq g (v))))$
9	5 8	mpbid	$⊢ φ \to (⋃ U \subseteq ⋃ V \land \exists g (g : V ⟶ U \land \forall v \in V v \subseteq g (v)))$
10	9	simprd	$⊢ φ \to \exists g (g : V ⟶ U \land \forall v \in V v \subseteq g (v))$
11		funmpt	$⊢ Fun (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
12	11	a1i	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to Fun (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
13		eqid	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
14	13	dmmptss	$⊢ dom (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq ran g$
15		frn	$⊢ g : V ⟶ U \to ran g \subseteq U$
16	15	ad2antlr	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ran g \subseteq U$
17	14 16	sstrid	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to dom (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq U$
18		locfintop	$⊢ V \in LocFin (J) \to J \in Top$
19	6 18	syl	$⊢ φ \to J \in Top$
20	19	ad3antrrr	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \to J \in Top$
21		cnvimass	$⊢ g^{-1} [\{u\}] \subseteq dom g$
22		fdm	$⊢ g : V ⟶ U \to dom g = V$
23	22	ad3antlr	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \to dom g = V$
24	21 23	sseqtrid	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \to g^{-1} [\{u\}] \subseteq V$
25	4	ad3antrrr	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \to V \subseteq J$
26	24 25	sstrd	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \to g^{-1} [\{u\}] \subseteq J$
27		uniopn	$⊢ (J \in Top \land g^{-1} [\{u\}] \subseteq J) \to ⋃ g^{-1} [\{u\}] \in J$
28	20 26 27	syl2anc	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \to ⋃ g^{-1} [\{u\}] \in J$
29	28	ralrimiva	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to \forall u \in ran g ⋃ g^{-1} [\{u\}] \in J$
30	13	rnmptss	$⊢ \forall u \in ran g ⋃ g^{-1} [\{u\}] \in J \to ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq J$
31	29 30	syl	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq J$
32		eqid	$⊢ ⋃ V = ⋃ V$
33		eqid	$⊢ ⋃ U = ⋃ U$
34	32 33	refbas	$⊢ V Ref U \to ⋃ U = ⋃ V$
35	5 34	syl	$⊢ φ \to ⋃ U = ⋃ V$
36	35	ad2antrr	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ⋃ U = ⋃ V$
37		nfv	$⊢ Ⅎ v (φ \land g : V ⟶ U)$
38		nfra1	$⊢ Ⅎ v \forall v \in V v \subseteq g (v)$
39	37 38	nfan	$⊢ Ⅎ v ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v))$
40		nfre1	$⊢ Ⅎ v \exists v \in V x \in v$
41	39 40	nfan	$⊢ Ⅎ v (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land \exists v \in V x \in v)$
42		ffn	$⊢ g : V ⟶ U \to g Fn V$
43	42	ad4antlr	$⊢ ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land v \in V) \land x \in v) \to g Fn V$
44		simplr	$⊢ ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land v \in V) \land x \in v) \to v \in V$
45		fnfvelrn	$⊢ (g Fn V \land v \in V) \to g (v) \in ran g$
46	43 44 45	syl2anc	$⊢ ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land v \in V) \land x \in v) \to g (v) \in ran g$
47		ssid	$⊢ v \subseteq v$
48	42	ad3antlr	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land v \in V) \to g Fn V$
49		eqid	$⊢ g (v) = g (v)$
50		fniniseg	$⊢ g Fn V \to (v \in g^{-1} [\{g (v)\}] \leftrightarrow (v \in V \land g (v) = g (v)))$
51	50	biimpar	$⊢ (g Fn V \land (v \in V \land g (v) = g (v))) \to v \in g^{-1} [\{g (v)\}]$
52	49 51	mpanr2	$⊢ (g Fn V \land v \in V) \to v \in g^{-1} [\{g (v)\}]$
53	48 52	sylancom	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land v \in V) \to v \in g^{-1} [\{g (v)\}]$
54		ssuni	$⊢ (v \subseteq v \land v \in g^{-1} [\{g (v)\}]) \to v \subseteq ⋃ g^{-1} [\{g (v)\}]$
55	47 53 54	sylancr	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land v \in V) \to v \subseteq ⋃ g^{-1} [\{g (v)\}]$
56	55	sselda	$⊢ ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land v \in V) \land x \in v) \to x \in ⋃ g^{-1} [\{g (v)\}]$
57		sneq	$⊢ u = g (v) \to \{u\} = \{g (v)\}$
58	57	imaeq2d	$⊢ u = g (v) \to g^{-1} [\{u\}] = g^{-1} [\{g (v)\}]$
59	58	unieqd	$⊢ u = g (v) \to ⋃ g^{-1} [\{u\}] = ⋃ g^{-1} [\{g (v)\}]$
60	59	eleq2d	$⊢ u = g (v) \to (x \in ⋃ g^{-1} [\{u\}] \leftrightarrow x \in ⋃ g^{-1} [\{g (v)\}])$
61	60	rspcev	$⊢ (g (v) \in ran g \land x \in ⋃ g^{-1} [\{g (v)\}]) \to \exists u \in ran g x \in ⋃ g^{-1} [\{u\}]$
62	46 56 61	syl2anc	$⊢ ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land v \in V) \land x \in v) \to \exists u \in ran g x \in ⋃ g^{-1} [\{u\}]$
63	62	adantllr	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land \exists v \in V x \in v) \land v \in V) \land x \in v) \to \exists u \in ran g x \in ⋃ g^{-1} [\{u\}]$
64		simpr	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land \exists v \in V x \in v) \to \exists v \in V x \in v$
65	41 63 64	r19.29af	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land \exists v \in V x \in v) \to \exists u \in ran g x \in ⋃ g^{-1} [\{u\}]$
66		nfv	$⊢ Ⅎ v u \in ran g$
67	39 66	nfan	$⊢ Ⅎ v (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g)$
68		nfv	$⊢ Ⅎ v x \in ⋃ g^{-1} [\{u\}]$
69	67 68	nfan	$⊢ Ⅎ v ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \land x \in ⋃ g^{-1} [\{u\}])$
70	24	ad3antrrr	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \land x \in ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \land x \in v) \to g^{-1} [\{u\}] \subseteq V$
71		simplr	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \land x \in ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \land x \in v) \to v \in g^{-1} [\{u\}]$
72	70 71	sseldd	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \land x \in ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \land x \in v) \to v \in V$
73		simpr	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \land x \in ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \land x \in v) \to x \in v$
74		simpr	$⊢ ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \land x \in ⋃ g^{-1} [\{u\}]) \to x \in ⋃ g^{-1} [\{u\}]$
75		eluni2	$⊢ x \in ⋃ g^{-1} [\{u\}] \leftrightarrow \exists v \in g^{-1} [\{u\}] x \in v$
76	74 75	sylib	$⊢ ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \land x \in ⋃ g^{-1} [\{u\}]) \to \exists v \in g^{-1} [\{u\}] x \in v$
77	69 72 73 76	reximd2a	$⊢ ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land u \in ran g) \land x \in ⋃ g^{-1} [\{u\}]) \to \exists v \in V x \in v$
78	77	r19.29an	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land \exists u \in ran g x \in ⋃ g^{-1} [\{u\}]) \to \exists v \in V x \in v$
79	65 78	impbida	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to (\exists v \in V x \in v \leftrightarrow \exists u \in ran g x \in ⋃ g^{-1} [\{u\}])$
80		eluni2	$⊢ x \in ⋃ V \leftrightarrow \exists v \in V x \in v$
81		eliun	$⊢ x \in ⋃_{u \in ran g} ⋃ g^{-1} [\{u\}] \leftrightarrow \exists u \in ran g x \in ⋃ g^{-1} [\{u\}]$
82	79 80 81	3bitr4g	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to (x \in ⋃ V \leftrightarrow x \in ⋃_{u \in ran g} ⋃ g^{-1} [\{u\}])$
83	82	eqrdv	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ⋃ V = ⋃_{u \in ran g} ⋃ g^{-1} [\{u\}]$
84		dfiun3g	$⊢ \forall u \in ran g ⋃ g^{-1} [\{u\}] \in J \to ⋃_{u \in ran g} ⋃ g^{-1} [\{u\}] = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
85	29 84	syl	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ⋃_{u \in ran g} ⋃ g^{-1} [\{u\}] = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
86	36 83 85	3eqtrd	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ⋃ U = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
87	15	ad3antlr	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \to ran g \subseteq U$
88		vex	$⊢ w \in V$
89	13	elrnmpt	$⊢ w \in V \to (w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \leftrightarrow \exists u \in ran g w = ⋃ g^{-1} [\{u\}])$
90	88 89	mp1i	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to (w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \leftrightarrow \exists u \in ran g w = ⋃ g^{-1} [\{u\}])$
91	90	biimpa	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \to \exists u \in ran g w = ⋃ g^{-1} [\{u\}]$
92		ssrexv	$⊢ ran g \subseteq U \to (\exists u \in ran g w = ⋃ g^{-1} [\{u\}] \to \exists u \in U w = ⋃ g^{-1} [\{u\}])$
93	87 91 92	sylc	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \to \exists u \in U w = ⋃ g^{-1} [\{u\}]$
94		nfv	$⊢ Ⅎ u ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v))$
95		nfmpt1	$⊢ \underline{Ⅎ} u (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
96	95	nfrn	$⊢ \underline{Ⅎ} u ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
97	96	nfcri	$⊢ Ⅎ u w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
98	94 97	nfan	$⊢ Ⅎ u (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]))$
99		simpr	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \to w = ⋃ g^{-1} [\{u\}]$
100		nfv	$⊢ Ⅎ v w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
101	39 100	nfan	$⊢ Ⅎ v (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]))$
102		nfv	$⊢ Ⅎ v u \in U$
103	101 102	nfan	$⊢ Ⅎ v ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U)$
104		nfv	$⊢ Ⅎ v w = ⋃ g^{-1} [\{u\}]$
105	103 104	nfan	$⊢ Ⅎ v (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}])$
106		simp-5r	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \to \forall v \in V v \subseteq g (v)$
107	42	ad5antlr	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \to g Fn V$
108		fniniseg	$⊢ g Fn V \to (v \in g^{-1} [\{u\}] \leftrightarrow (v \in V \land g (v) = u))$
109	107 108	syl	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \to (v \in g^{-1} [\{u\}] \leftrightarrow (v \in V \land g (v) = u))$
110	109	biimpa	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \to (v \in V \land g (v) = u)$
111	110	simpld	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \to v \in V$
112		rspa	$⊢ (\forall v \in V v \subseteq g (v) \land v \in V) \to v \subseteq g (v)$
113	106 111 112	syl2anc	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \to v \subseteq g (v)$
114	110	simprd	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \to g (v) = u$
115	113 114	sseqtrd	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \land v \in g^{-1} [\{u\}]) \to v \subseteq u$
116	115	ex	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \to (v \in g^{-1} [\{u\}] \to v \subseteq u)$
117	105 116	ralrimi	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \to \forall v \in g^{-1} [\{u\}] v \subseteq u$
118		unissb	$⊢ ⋃ g^{-1} [\{u\}] \subseteq u \leftrightarrow \forall v \in g^{-1} [\{u\}] v \subseteq u$
119	117 118	sylibr	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \to ⋃ g^{-1} [\{u\}] \subseteq u$
120	99 119	eqsstrd	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \land u \in U) \land w = ⋃ g^{-1} [\{u\}]) \to w \subseteq u$
121	120	exp31	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \to (u \in U \to (w = ⋃ g^{-1} [\{u\}] \to w \subseteq u))$
122	98 121	reximdai	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \to (\exists u \in U w = ⋃ g^{-1} [\{u\}] \to \exists u \in U w \subseteq u)$
123	93 122	mpd	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])) \to \exists u \in U w \subseteq u$
124	123	ralrimiva	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to \forall w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \exists u \in U w \subseteq u$
125		vex	$⊢ g \in V$
126	125	rnex	$⊢ ran g \in V$
127	126	mptex	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in V$
128		rnexg	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in V \to ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in V$
129	127 128	mp1i	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in V$
130		eqid	$⊢ ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
131	130 33	isref	$⊢ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in V \to (ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Ref U \leftrightarrow (⋃ U = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \land \forall w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \exists u \in U w \subseteq u))$
132	129 131	syl	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to (ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Ref U \leftrightarrow (⋃ U = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \land \forall w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \exists u \in U w \subseteq u))$
133	86 124 132	mpbir2and	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Ref U$
134	19	ad2antrr	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to J \in Top$
135	3	ad2antrr	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to X = ⋃ U$
136	135 86	eqtrd	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to X = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
137		nfv	$⊢ Ⅎ v x \in X$
138	39 137	nfan	$⊢ Ⅎ v (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X)$
139		simplr	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land (x \in v \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin)) \to v \in J$
140		ffun	$⊢ g : V ⟶ U \to Fun g$
141	140	ad6antlr	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to Fun g$
142		imafi	$⊢ (Fun g \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to g [\{j \in V \| j \cap v \neq \emptyset\}] \in Fin$
143	141 142	sylancom	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to g [\{j \in V \| j \cap v \neq \emptyset\}] \in Fin$
144		simp3	$⊢ (((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land k \in ran g \land w = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) (k)) \to w = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) (k)$
145		sneq	$⊢ u = k \to \{u\} = \{k\}$
146	145	imaeq2d	$⊢ u = k \to g^{-1} [\{u\}] = g^{-1} [\{k\}]$
147	146	unieqd	$⊢ u = k \to ⋃ g^{-1} [\{u\}] = ⋃ g^{-1} [\{k\}]$
148	125	cnvex	$⊢ g^{-1} \in V$
149		imaexg	$⊢ g^{-1} \in V \to g^{-1} [\{k\}] \in V$
150	148 149	ax-mp	$⊢ g^{-1} [\{k\}] \in V$
151	150	uniex	$⊢ ⋃ g^{-1} [\{k\}] \in V$
152	147 13 151	fvmpt	$⊢ k \in ran g \to (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) (k) = ⋃ g^{-1} [\{k\}]$
153	152	3ad2ant2	$⊢ (((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land k \in ran g \land w = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) (k)) \to (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) (k) = ⋃ g^{-1} [\{k\}]$
154	144 153	eqtrd	$⊢ (((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land k \in ran g \land w = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) (k)) \to w = ⋃ g^{-1} [\{k\}]$
155	154	ineq1d	$⊢ (((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land k \in ran g \land w = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) (k)) \to w \cap v = ⋃ g^{-1} [\{k\}] \cap v$
156	155	neeq1d	$⊢ (((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land k \in ran g \land w = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) (k)) \to (w \cap v \neq \emptyset \leftrightarrow ⋃ g^{-1} [\{k\}] \cap v \neq \emptyset)$
157	126	a1i	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to ran g \in V$
158		imaexg	$⊢ g^{-1} \in V \to g^{-1} [\{u\}] \in V$
159	148 158	ax-mp	$⊢ g^{-1} [\{u\}] \in V$
160	159	uniex	$⊢ ⋃ g^{-1} [\{u\}] \in V$
161	160 13	fnmpti	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Fn ran g$
162		dffn4	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Fn ran g \leftrightarrow (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) : ran g \underset{onto}{⟶} ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
163	161 162	mpbi	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) : ran g \underset{onto}{⟶} ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
164	163	a1i	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) : ran g \underset{onto}{⟶} ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
165	156 157 164	rabfodom	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} ≼ \{k \in ran g \| ⋃ g^{-1} [\{k\}] \cap v \neq \emptyset\}$
166		sneq	$⊢ k = u \to \{k\} = \{u\}$
167	166	imaeq2d	$⊢ k = u \to g^{-1} [\{k\}] = g^{-1} [\{u\}]$
168	167	unieqd	$⊢ k = u \to ⋃ g^{-1} [\{k\}] = ⋃ g^{-1} [\{u\}]$
169	168	ineq1d	$⊢ k = u \to ⋃ g^{-1} [\{k\}] \cap v = ⋃ g^{-1} [\{u\}] \cap v$
170	169	neeq1d	$⊢ k = u \to (⋃ g^{-1} [\{k\}] \cap v \neq \emptyset \leftrightarrow ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset)$
171	170	cbvrabv	$⊢ \{k \in ran g \| ⋃ g^{-1} [\{k\}] \cap v \neq \emptyset\} = \{u \in ran g \| ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset\}$
172	165 171	breqtrdi	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} ≼ \{u \in ran g \| ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset\}$
173	126	rabex	$⊢ \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\} \in V$
174		nfv	$⊢ Ⅎ j (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v)$
175		nfrab1	$⊢ \underline{Ⅎ} j \{j \in V \| j \cap v \neq \emptyset\}$
176	175	nfel1	$⊢ Ⅎ j \{j \in V \| j \cap v \neq \emptyset\} \in Fin$
177	174 176	nfan	$⊢ Ⅎ j ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin)$
178		nfv	$⊢ Ⅎ j u \in ran g$
179	177 178	nfan	$⊢ Ⅎ j (((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g)$
180		nfv	$⊢ Ⅎ j ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset$
181	179 180	nfan	$⊢ Ⅎ j ((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset)$
182		nfv	$⊢ Ⅎ j g (k) = u$
183	175 182	nfrexw	$⊢ Ⅎ j \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u$
184	42	ad5antlr	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \to g Fn V$
185	184	ad5antr	$⊢ ((((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \land j \in g^{-1} [\{u\}]) \land j \cap v \neq \emptyset) \to g Fn V$
186		simplr	$⊢ ((((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \land j \in g^{-1} [\{u\}]) \land j \cap v \neq \emptyset) \to j \in g^{-1} [\{u\}]$
187		fniniseg	$⊢ g Fn V \to (j \in g^{-1} [\{u\}] \leftrightarrow (j \in V \land g (j) = u))$
188	187	biimpa	$⊢ (g Fn V \land j \in g^{-1} [\{u\}]) \to (j \in V \land g (j) = u)$
189	185 186 188	syl2anc	$⊢ ((((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \land j \in g^{-1} [\{u\}]) \land j \cap v \neq \emptyset) \to (j \in V \land g (j) = u)$
190	189	simpld	$⊢ ((((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \land j \in g^{-1} [\{u\}]) \land j \cap v \neq \emptyset) \to j \in V$
191		simpr	$⊢ ((((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \land j \in g^{-1} [\{u\}]) \land j \cap v \neq \emptyset) \to j \cap v \neq \emptyset$
192		rabid	$⊢ j \in \{j \in V \| j \cap v \neq \emptyset\} \leftrightarrow (j \in V \land j \cap v \neq \emptyset)$
193	190 191 192	sylanbrc	$⊢ ((((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \land j \in g^{-1} [\{u\}]) \land j \cap v \neq \emptyset) \to j \in \{j \in V \| j \cap v \neq \emptyset\}$
194	189	simprd	$⊢ ((((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \land j \in g^{-1} [\{u\}]) \land j \cap v \neq \emptyset) \to g (j) = u$
195		fveqeq2	$⊢ k = j \to (g (k) = u \leftrightarrow g (j) = u)$
196	195	rspcev	$⊢ (j \in \{j \in V \| j \cap v \neq \emptyset\} \land g (j) = u) \to \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u$
197	193 194 196	syl2anc	$⊢ ((((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \land j \in g^{-1} [\{u\}]) \land j \cap v \neq \emptyset) \to \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u$
198		uniinn0	$⊢ ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset \leftrightarrow \exists j \in g^{-1} [\{u\}] j \cap v \neq \emptyset$
199	198	biimpi	$⊢ ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset \to \exists j \in g^{-1} [\{u\}] j \cap v \neq \emptyset$
200	199	adantl	$⊢ ((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \to \exists j \in g^{-1} [\{u\}] j \cap v \neq \emptyset$
201	181 183 197 200	r19.29af2	$⊢ ((((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \land ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset) \to \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u$
202	201	ex	$⊢ (((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \land u \in ran g) \to (⋃ g^{-1} [\{u\}] \cap v \neq \emptyset \to \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u)$
203	202	ss2rabdv	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to \{u \in ran g \| ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset\} \subseteq \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\}$
204		ssdomg	$⊢ \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\} \in V \to (\{u \in ran g \| ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset\} \subseteq \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\} \to \{u \in ran g \| ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset\} ≼ \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\})$
205	173 203 204	mpsyl	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to \{u \in ran g \| ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset\} ≼ \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\}$
206		domtr	$⊢ (\{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} ≼ \{u \in ran g \| ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset\} \land \{u \in ran g \| ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset\} ≼ \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\}) \to \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} ≼ \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\}$
207	172 205 206	syl2anc	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} ≼ \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\}$
208	184	adantr	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to g Fn V$
209		dffn3	$⊢ g Fn V \leftrightarrow g : V ⟶ ran g$
210	209	biimpi	$⊢ g Fn V \to g : V ⟶ ran g$
211		ssrab2	$⊢ \{j \in V \| j \cap v \neq \emptyset\} \subseteq V$
212		fimarab	$⊢ (g : V ⟶ ran g \land \{j \in V \| j \cap v \neq \emptyset\} \subseteq V) \to g [\{j \in V \| j \cap v \neq \emptyset\}] = \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\}$
213	211 212	mpan2	$⊢ g : V ⟶ ran g \to g [\{j \in V \| j \cap v \neq \emptyset\}] = \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\}$
214	208 210 213	3syl	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to g [\{j \in V \| j \cap v \neq \emptyset\}] = \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\}$
215	207 214	breqtrrd	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} ≼ g [\{j \in V \| j \cap v \neq \emptyset\}]$
216		domfi	$⊢ (g [\{j \in V \| j \cap v \neq \emptyset\}] \in Fin \land \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} ≼ g [\{j \in V \| j \cap v \neq \emptyset\}]) \to \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} \in Fin$
217	143 215 216	syl2anc	$⊢ ((((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} \in Fin$
218	217	ex	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land x \in v) \to (\{j \in V \| j \cap v \neq \emptyset\} \in Fin \to \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} \in Fin)$
219	218	imdistanda	$⊢ ((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \to ((x \in v \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin) \to (x \in v \land \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} \in Fin))$
220	219	imp	$⊢ (((((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \land v \in J) \land (x \in v \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin)) \to (x \in v \land \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} \in Fin)$
221		simplll	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \to φ$
222	1 32	islocfin	$⊢ V \in LocFin (J) \leftrightarrow (J \in Top \land X = ⋃ V \land \forall x \in X \exists v \in J (x \in v \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin))$
223	6 222	sylib	$⊢ φ \to (J \in Top \land X = ⋃ V \land \forall x \in X \exists v \in J (x \in v \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin))$
224	223	simp3d	$⊢ φ \to \forall x \in X \exists v \in J (x \in v \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin)$
225	224	r19.21bi	$⊢ (φ \land x \in X) \to \exists v \in J (x \in v \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin)$
226	221 225	sylancom	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \to \exists v \in J (x \in v \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin)$
227	138 139 220 226	reximd2a	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \to \exists v \in J (x \in v \land \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} \in Fin)$
228	227	ralrimiva	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to \forall x \in X \exists v \in J (x \in v \land \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} \in Fin)$
229	1 130	islocfin	$⊢ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in LocFin (J) \leftrightarrow (J \in Top \land X = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \land \forall x \in X \exists v \in J (x \in v \land \{w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \| w \cap v \neq \emptyset\} \in Fin))$
230	134 136 228 229	syl3anbrc	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in LocFin (J)$
231		funeq	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to (Fun f \leftrightarrow Fun (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]))$
232		dmeq	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to dom f = dom (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
233	232	sseq1d	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to (dom f \subseteq U \leftrightarrow dom (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq U)$
234		rneq	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to ran f = ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
235	234	sseq1d	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to (ran f \subseteq J \leftrightarrow ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq J)$
236	231 233 235	3anbi123d	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to ((Fun f \land dom f \subseteq U \land ran f \subseteq J) \leftrightarrow (Fun (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \land dom (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq U \land ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq J))$
237	234	breq1d	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to (ran f Ref U \leftrightarrow ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Ref U)$
238	234	eleq1d	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to (ran f \in LocFin (J) \leftrightarrow ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in LocFin (J))$
239	237 238	anbi12d	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to ((ran f Ref U \land ran f \in LocFin (J)) \leftrightarrow (ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Ref U \land ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in LocFin (J)))$
240	236 239	anbi12d	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to (((Fun f \land dom f \subseteq U \land ran f \subseteq J) \land (ran f Ref U \land ran f \in LocFin (J))) \leftrightarrow ((Fun (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \land dom (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq U \land ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq J) \land (ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Ref U \land ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in LocFin (J))))$
241	127 240	spcev	$⊢ ((Fun (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \land dom (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq U \land ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \subseteq J) \land (ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Ref U \land ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in LocFin (J))) \to \exists f ((Fun f \land dom f \subseteq U \land ran f \subseteq J) \land (ran f Ref U \land ran f \in LocFin (J)))$
242	12 17 31 133 230 241	syl32anc	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to \exists f ((Fun f \land dom f \subseteq U \land ran f \subseteq J) \land (ran f Ref U \land ran f \in LocFin (J)))$
243	242	expl	$⊢ φ \to ((g : V ⟶ U \land \forall v \in V v \subseteq g (v)) \to \exists f ((Fun f \land dom f \subseteq U \land ran f \subseteq J) \land (ran f Ref U \land ran f \in LocFin (J))))$
244	243	exlimdv	$⊢ φ \to (\exists g (g : V ⟶ U \land \forall v \in V v \subseteq g (v)) \to \exists f ((Fun f \land dom f \subseteq U \land ran f \subseteq J) \land (ran f Ref U \land ran f \in LocFin (J))))$
245	10 244	mpd	$⊢ φ \to \exists f ((Fun f \land dom f \subseteq U \land ran f \subseteq J) \land (ran f Ref U \land ran f \in LocFin (J)))$

Metamath Proof Explorer

Theorem locfinreflem

Proof