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		eluni2	$⊢ x \in ⋃ g^{-1} [\{u\}] \leftrightarrow \exists v \in g^{-1} [\{u\}] x \in v$
75	74	bilani	$⊢ ((((φ \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$
76	69 72 73 75	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$
77	76	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$
78	65 77	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\}])$
79		eluni2	$⊢ x \in ⋃ V \leftrightarrow \exists v \in V x \in v$
80		eliun	$⊢ x \in ⋃_{u \in ran g} ⋃ g^{-1} [\{u\}] \leftrightarrow \exists u \in ran g x \in ⋃ g^{-1} [\{u\}]$
81	78 79 80	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\}])$
82	81	eqrdv	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ⋃ V = ⋃_{u \in ran g} ⋃ g^{-1} [\{u\}]$
83		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\}])$
84	29 83	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\}])$
85	36 82 84	3eqtrd	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to ⋃ U = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
86	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$
87		vex	$⊢ w \in V$
88	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\}])$
89	87 88	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\}])$
90	89	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\}]$
91		ssrexv	$⊢ ran g \subseteq U \to (\exists u \in ran g w = ⋃ g^{-1} [\{u\}] \to \exists u \in U w = ⋃ g^{-1} [\{u\}])$
92	86 90 91	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\}]$
93		nfv	$⊢ Ⅎ u ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v))$
94		nfmpt1	$⊢ \underline{Ⅎ} u (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
95	94	nfrn	$⊢ \underline{Ⅎ} u ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
96	95	nfcri	$⊢ Ⅎ u w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
97	93 96	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\}]))$
98		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\}]$
99		nfv	$⊢ Ⅎ v w \in ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
100	39 99	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\}]))$
101		nfv	$⊢ Ⅎ v u \in U$
102	100 101	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)$
103		nfv	$⊢ Ⅎ v w = ⋃ g^{-1} [\{u\}]$
104	102 103	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\}])$
105		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)$
106	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$
107		fniniseg	$⊢ g Fn V \to (v \in g^{-1} [\{u\}] \leftrightarrow (v \in V \land g (v) = u))$
108	106 107	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))$
109	108	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)$
110	109	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$
111		rspa	$⊢ (\forall v \in V v \subseteq g (v) \land v \in V) \to v \subseteq g (v)$
112	105 110 111	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)$
113	109	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$
114	112 113	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$
115	114	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)$
116	104 115	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$
117		unissb	$⊢ ⋃ g^{-1} [\{u\}] \subseteq u \leftrightarrow \forall v \in g^{-1} [\{u\}] v \subseteq u$
118	116 117	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$
119	98 118	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$
120	119	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))$
121	97 120	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)$
122	92 121	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$
123	122	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$
124		vex	$⊢ g \in V$
125	124	rnex	$⊢ ran g \in V$
126	125	mptex	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in V$
127		rnexg	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in V \to ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \in V$
128	126 127	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$
129		eqid	$⊢ ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
130	129 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))$
131	128 130	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))$
132	85 123 131	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$
133	19	ad2antrr	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to J \in Top$
134	3	ad2antrr	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to X = ⋃ U$
135	134 85	eqtrd	$⊢ ((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \to X = ⋃ ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
136		nfv	$⊢ Ⅎ v x \in X$
137	39 136	nfan	$⊢ Ⅎ v (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X)$
138		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$
139		ffun	$⊢ g : V ⟶ U \to Fun g$
140	139	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$
141		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$
142	140 141	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$
143		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)$
144		sneq	$⊢ u = k \to \{u\} = \{k\}$
145	144	imaeq2d	$⊢ u = k \to g^{-1} [\{u\}] = g^{-1} [\{k\}]$
146	145	unieqd	$⊢ u = k \to ⋃ g^{-1} [\{u\}] = ⋃ g^{-1} [\{k\}]$
147	124	cnvex	$⊢ g^{-1} \in V$
148		imaexg	$⊢ g^{-1} \in V \to g^{-1} [\{k\}] \in V$
149	147 148	ax-mp	$⊢ g^{-1} [\{k\}] \in V$
150	149	uniex	$⊢ ⋃ g^{-1} [\{k\}] \in V$
151	146 13 150	fvmpt	$⊢ k \in ran g \to (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) (k) = ⋃ g^{-1} [\{k\}]$
152	151	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\}]$
153	143 152	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\}]$
154	153	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$
155	154	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)$
156	125	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$
157		imaexg	$⊢ g^{-1} \in V \to g^{-1} [\{u\}] \in V$
158	147 157	ax-mp	$⊢ g^{-1} [\{u\}] \in V$
159	158	uniex	$⊢ ⋃ g^{-1} [\{u\}] \in V$
160	159 13	fnmpti	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) Fn ran g$
161		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\}])$
162	160 161	mpbi	$⊢ (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) : ran g \underset{onto}{⟶} ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
163	162	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\}])$
164	155 156 163	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\}$
165		sneq	$⊢ k = u \to \{k\} = \{u\}$
166	165	imaeq2d	$⊢ k = u \to g^{-1} [\{k\}] = g^{-1} [\{u\}]$
167	166	unieqd	$⊢ k = u \to ⋃ g^{-1} [\{k\}] = ⋃ g^{-1} [\{u\}]$
168	167	ineq1d	$⊢ k = u \to ⋃ g^{-1} [\{k\}] \cap v = ⋃ g^{-1} [\{u\}] \cap v$
169	168	neeq1d	$⊢ k = u \to (⋃ g^{-1} [\{k\}] \cap v \neq \emptyset \leftrightarrow ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset)$
170	169	cbvrabv	$⊢ \{k \in ran g \| ⋃ g^{-1} [\{k\}] \cap v \neq \emptyset\} = \{u \in ran g \| ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset\}$
171	164 170	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\}$
172	125	rabex	$⊢ \{u \in ran g \| \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u\} \in V$
173		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)$
174		nfrab1	$⊢ \underline{Ⅎ} j \{j \in V \| j \cap v \neq \emptyset\}$
175	174	nfel1	$⊢ Ⅎ j \{j \in V \| j \cap v \neq \emptyset\} \in Fin$
176	173 175	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)$
177		nfv	$⊢ Ⅎ j u \in ran g$
178	176 177	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)$
179		nfv	$⊢ Ⅎ j ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset$
180	178 179	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)$
181		nfv	$⊢ Ⅎ j g (k) = u$
182	174 181	nfrexw	$⊢ Ⅎ j \exists k \in \{j \in V \| j \cap v \neq \emptyset\} g (k) = u$
183	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$
184	183	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$
185		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\}]$
186		fniniseg	$⊢ g Fn V \to (j \in g^{-1} [\{u\}] \leftrightarrow (j \in V \land g (j) = u))$
187	186	biimpa	$⊢ (g Fn V \land j \in g^{-1} [\{u\}]) \to (j \in V \land g (j) = u)$
188	184 185 187	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)$
189	188	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$
190		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$
191		rabid	$⊢ j \in \{j \in V \| j \cap v \neq \emptyset\} \leftrightarrow (j \in V \land j \cap v \neq \emptyset)$
192	189 190 191	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\}$
193	188	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$
194		fveqeq2	$⊢ k = j \to (g (k) = u \leftrightarrow g (j) = u)$
195	194	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$
196	192 193 195	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$
197		uniinn0	$⊢ ⋃ g^{-1} [\{u\}] \cap v \neq \emptyset \leftrightarrow \exists j \in g^{-1} [\{u\}] j \cap v \neq \emptyset$
198	197	bilani	$⊢ ((((((((φ \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$
199	180 182 196 198	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$
200	199	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)$
201	200	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\}$
202		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\})$
203	172 201 202	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\}$
204		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\}$
205	171 203 204	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\}$
206	183	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$
207		dffn3	$⊢ g Fn V \leftrightarrow g : V ⟶ ran g$
208	207	biimpi	$⊢ g Fn V \to g : V ⟶ ran g$
209		ssrab2	$⊢ \{j \in V \| j \cap v \neq \emptyset\} \subseteq V$
210		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\}$
211	209 210	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\}$
212	206 208 211	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\}$
213	205 212	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\}]$
214		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$
215	142 213 214	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$
216	215	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)$
217	216	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))$
218	217	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)$
219		simplll	$⊢ (((φ \land g : V ⟶ U) \land \forall v \in V v \subseteq g (v)) \land x \in X) \to φ$
220	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))$
221	6 220	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))$
222	221	simp3d	$⊢ φ \to \forall x \in X \exists v \in J (x \in v \land \{j \in V \| j \cap v \neq \emptyset\} \in Fin)$
223	222	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)$
224	219 223	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)$
225	137 138 218 224	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)$
226	225	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)$
227	1 129	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))$
228	133 135 226 227	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)$
229		funeq	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to (Fun f \leftrightarrow Fun (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]))$
230		dmeq	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to dom f = dom (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
231	230	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)$
232		rneq	$⊢ f = (u \in ran g ⟼ ⋃ g^{-1} [\{u\}]) \to ran f = ran (u \in ran g ⟼ ⋃ g^{-1} [\{u\}])$
233	232	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)$
234	229 231 233	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))$
235	232	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)$
236	232	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))$
237	235 236	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)))$
238	234 237	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))))$
239	126 238	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)))$
240	12 17 31 132 228 239	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)))$
241	240	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))))$
242	241	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))))$
243	10 242	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