locfinref

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. (Contributed by Thierry Arnoux, 31-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	locfinref	$⊢ φ \to \exists f (f : U ⟶ 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		f0	$⊢ \emptyset : \emptyset ⟶ J$
8		simpr	$⊢ (φ \land U = \emptyset) \to U = \emptyset$
9	8	feq2d	$⊢ (φ \land U = \emptyset) \to (\emptyset : U ⟶ J \leftrightarrow \emptyset : \emptyset ⟶ J)$
10	7 9	mpbiri	$⊢ (φ \land U = \emptyset) \to \emptyset : U ⟶ J$
11		rn0	$⊢ ran \emptyset = \emptyset$
12		0ex	$⊢ \emptyset \in V$
13		refref	$⊢ \emptyset \in V \to \emptyset Ref \emptyset$
14	12 13	ax-mp	$⊢ \emptyset Ref \emptyset$
15	11 14	eqbrtri	$⊢ ran \emptyset Ref \emptyset$
16	15 8	breqtrrid	$⊢ (φ \land U = \emptyset) \to ran \emptyset Ref U$
17		sn0top	$⊢ \{\emptyset\} \in Top$
18	17	a1i	$⊢ (φ \land U = \emptyset) \to \{\emptyset\} \in Top$
19		eqidd	$⊢ (φ \land U = \emptyset) \to \emptyset = \emptyset$
20		ral0	$⊢ \forall x \in \emptyset \exists n \in \{\emptyset\} (x \in n \land \{s \in ran \emptyset \| s \cap n \neq \emptyset\} \in Fin)$
21	20	a1i	$⊢ (φ \land U = \emptyset) \to \forall x \in \emptyset \exists n \in \{\emptyset\} (x \in n \land \{s \in ran \emptyset \| s \cap n \neq \emptyset\} \in Fin)$
22	12	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
23	22	eqcomi	$⊢ \emptyset = ⋃ \{\emptyset\}$
24	11	unieqi	$⊢ ⋃ ran \emptyset = ⋃ \emptyset$
25		uni0	$⊢ ⋃ \emptyset = \emptyset$
26	24 25	eqtr2i	$⊢ \emptyset = ⋃ ran \emptyset$
27	23 26	islocfin	$⊢ ran \emptyset \in LocFin (\{\emptyset\}) \leftrightarrow (\{\emptyset\} \in Top \land \emptyset = \emptyset \land \forall x \in \emptyset \exists n \in \{\emptyset\} (x \in n \land \{s \in ran \emptyset \| s \cap n \neq \emptyset\} \in Fin))$
28	18 19 21 27	syl3anbrc	$⊢ (φ \land U = \emptyset) \to ran \emptyset \in LocFin (\{\emptyset\})$
29	3	adantr	$⊢ (φ \land U = \emptyset) \to X = ⋃ U$
30	8	unieqd	$⊢ (φ \land U = \emptyset) \to ⋃ U = ⋃ \emptyset$
31	29 30	eqtrd	$⊢ (φ \land U = \emptyset) \to X = ⋃ \emptyset$
32	31 1 25	3eqtr3g	$⊢ (φ \land U = \emptyset) \to ⋃ J = \emptyset$
33		locfintop	$⊢ V \in LocFin (J) \to J \in Top$
34		0top	$⊢ J \in Top \to (⋃ J = \emptyset \leftrightarrow J = \{\emptyset\})$
35	6 33 34	3syl	$⊢ φ \to (⋃ J = \emptyset \leftrightarrow J = \{\emptyset\})$
36	35	adantr	$⊢ (φ \land U = \emptyset) \to (⋃ J = \emptyset \leftrightarrow J = \{\emptyset\})$
37	32 36	mpbid	$⊢ (φ \land U = \emptyset) \to J = \{\emptyset\}$
38	37	fveq2d	$⊢ (φ \land U = \emptyset) \to LocFin (J) = LocFin (\{\emptyset\})$
39	28 38	eleqtrrd	$⊢ (φ \land U = \emptyset) \to ran \emptyset \in LocFin (J)$
40		feq1	$⊢ f = \emptyset \to (f : U ⟶ J \leftrightarrow \emptyset : U ⟶ J)$
41		rneq	$⊢ f = \emptyset \to ran f = ran \emptyset$
42	41	breq1d	$⊢ f = \emptyset \to (ran f Ref U \leftrightarrow ran \emptyset Ref U)$
43	41	eleq1d	$⊢ f = \emptyset \to (ran f \in LocFin (J) \leftrightarrow ran \emptyset \in LocFin (J))$
44	40 42 43	3anbi123d	$⊢ f = \emptyset \to ((f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J)) \leftrightarrow (\emptyset : U ⟶ J \land ran \emptyset Ref U \land ran \emptyset \in LocFin (J)))$
45	12 44	spcev	$⊢ (\emptyset : U ⟶ J \land ran \emptyset Ref U \land ran \emptyset \in LocFin (J)) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J))$
46	10 16 39 45	syl3anc	$⊢ (φ \land U = \emptyset) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J))$
47	1 2 3 4 5 6	locfinreflem	$⊢ φ \to \exists g ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))$
48	47	adantr	$⊢ (φ \land U \neq \emptyset) \to \exists g ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))$
49		simpl	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to (φ \land U \neq \emptyset)$
50		simprl1	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to Fun g$
51		fdmrn	$⊢ Fun g \leftrightarrow g : dom g ⟶ ran g$
52	50 51	sylib	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to g : dom g ⟶ ran g$
53		simprl3	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to ran g \subseteq J$
54	52 53	fssd	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to g : dom g ⟶ J$
55		fconstg	$⊢ \emptyset \in V \to ((U ∖ dom g) \times \{\emptyset\}) : U ∖ dom g ⟶ \{\emptyset\}$
56	12 55	mp1i	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to ((U ∖ dom g) \times \{\emptyset\}) : U ∖ dom g ⟶ \{\emptyset\}$
57		0opn	$⊢ J \in Top \to \emptyset \in J$
58	6 33 57	3syl	$⊢ φ \to \emptyset \in J$
59	58	ad2antrr	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to \emptyset \in J$
60	59	snssd	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to \{\emptyset\} \subseteq J$
61	56 60	fssd	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to ((U ∖ dom g) \times \{\emptyset\}) : U ∖ dom g ⟶ J$
62		disjdif	$⊢ dom g \cap (U ∖ dom g) = \emptyset$
63	62	a1i	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to dom g \cap (U ∖ dom g) = \emptyset$
64		fun2	$⊢ ((g : dom g ⟶ J \land ((U ∖ dom g) \times \{\emptyset\}) : U ∖ dom g ⟶ J) \land dom g \cap (U ∖ dom g) = \emptyset) \to (g \cup ((U ∖ dom g) \times \{\emptyset\})) : dom g \cup (U ∖ dom g) ⟶ J$
65	54 61 63 64	syl21anc	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to (g \cup ((U ∖ dom g) \times \{\emptyset\})) : dom g \cup (U ∖ dom g) ⟶ J$
66		simprl2	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to dom g \subseteq U$
67		undif	$⊢ dom g \subseteq U \leftrightarrow dom g \cup (U ∖ dom g) = U$
68	66 67	sylib	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to dom g \cup (U ∖ dom g) = U$
69	68	feq2d	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to ((g \cup ((U ∖ dom g) \times \{\emptyset\})) : dom g \cup (U ∖ dom g) ⟶ J \leftrightarrow (g \cup ((U ∖ dom g) \times \{\emptyset\})) : U ⟶ J)$
70	65 69	mpbid	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to (g \cup ((U ∖ dom g) \times \{\emptyset\})) : U ⟶ J$
71		simpr	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g) \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g$
72		simprrl	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to ran g Ref U$
73	72	adantr	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g) \to ran g Ref U$
74	71 73	eqbrtrd	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g) \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) Ref U$
75		simpr	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}$
76	49	simprd	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to U \neq \emptyset$
77		refun0	$⊢ (ran g Ref U \land U \neq \emptyset) \to (ran g \cup \{\emptyset\}) Ref U$
78	72 76 77	syl2anc	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to (ran g \cup \{\emptyset\}) Ref U$
79	78	adantr	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to (ran g \cup \{\emptyset\}) Ref U$
80	75 79	eqbrtrd	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) Ref U$
81		rnxpss	$⊢ ran ((U ∖ dom g) \times \{\emptyset\}) \subseteq \{\emptyset\}$
82		sssn	$⊢ ran ((U ∖ dom g) \times \{\emptyset\}) \subseteq \{\emptyset\} \leftrightarrow (ran ((U ∖ dom g) \times \{\emptyset\}) = \emptyset \lor ran ((U ∖ dom g) \times \{\emptyset\}) = \{\emptyset\})$
83	81 82	mpbi	$⊢ (ran ((U ∖ dom g) \times \{\emptyset\}) = \emptyset \lor ran ((U ∖ dom g) \times \{\emptyset\}) = \{\emptyset\})$
84		rnun	$⊢ ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup ran ((U ∖ dom g) \times \{\emptyset\})$
85		uneq2	$⊢ ran ((U ∖ dom g) \times \{\emptyset\}) = \emptyset \to ran g \cup ran ((U ∖ dom g) \times \{\emptyset\}) = ran g \cup \emptyset$
86	84 85	syl5eq	$⊢ ran ((U ∖ dom g) \times \{\emptyset\}) = \emptyset \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \emptyset$
87		un0	$⊢ ran g \cup \emptyset = ran g$
88	86 87	eqtrdi	$⊢ ran ((U ∖ dom g) \times \{\emptyset\}) = \emptyset \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g$
89		uneq2	$⊢ ran ((U ∖ dom g) \times \{\emptyset\}) = \{\emptyset\} \to ran g \cup ran ((U ∖ dom g) \times \{\emptyset\}) = ran g \cup \{\emptyset\}$
90	84 89	syl5eq	$⊢ ran ((U ∖ dom g) \times \{\emptyset\}) = \{\emptyset\} \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}$
91	88 90	orim12i	$⊢ (ran ((U ∖ dom g) \times \{\emptyset\}) = \emptyset \lor ran ((U ∖ dom g) \times \{\emptyset\}) = \{\emptyset\}) \to (ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \lor ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\})$
92	83 91	mp1i	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to (ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \lor ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\})$
93	74 80 92	mpjaodan	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) Ref U$
94		simprrr	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to ran g \in LocFin (J)$
95	94	adantr	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g) \to ran g \in LocFin (J)$
96	71 95	eqeltrd	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g) \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) \in LocFin (J)$
97	94	adantr	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to ran g \in LocFin (J)$
98		snfi	$⊢ \{\emptyset\} \in Fin$
99	98	a1i	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to \{\emptyset\} \in Fin$
100	59	adantr	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to \emptyset \in J$
101	100	snssd	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to \{\emptyset\} \subseteq J$
102	101	unissd	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to ⋃ \{\emptyset\} \subseteq ⋃ J$
103		lfinun	$⊢ (ran g \in LocFin (J) \land \{\emptyset\} \in Fin \land ⋃ \{\emptyset\} \subseteq ⋃ J) \to ran g \cup \{\emptyset\} \in LocFin (J)$
104	97 99 102 103	syl3anc	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to ran g \cup \{\emptyset\} \in LocFin (J)$
105	75 104	eqeltrd	$⊢ (((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) = ran g \cup \{\emptyset\}) \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) \in LocFin (J)$
106	96 105 92	mpjaodan	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) \in LocFin (J)$
107		refrel	$⊢ Rel Ref$
108	107	brrelex2i	$⊢ V Ref U \to U \in V$
109		difexg	$⊢ U \in V \to U ∖ dom g \in V$
110	5 108 109	3syl	$⊢ φ \to U ∖ dom g \in V$
111	110	adantr	$⊢ (φ \land U \neq \emptyset) \to U ∖ dom g \in V$
112		p0ex	$⊢ \{\emptyset\} \in V$
113		xpexg	$⊢ (U ∖ dom g \in V \land \{\emptyset\} \in V) \to (U ∖ dom g) \times \{\emptyset\} \in V$
114	112 113	mpan2	$⊢ U ∖ dom g \in V \to (U ∖ dom g) \times \{\emptyset\} \in V$
115		vex	$⊢ g \in V$
116		unexg	$⊢ (g \in V \land (U ∖ dom g) \times \{\emptyset\} \in V) \to g \cup ((U ∖ dom g) \times \{\emptyset\}) \in V$
117	115 116	mpan	$⊢ (U ∖ dom g) \times \{\emptyset\} \in V \to g \cup ((U ∖ dom g) \times \{\emptyset\}) \in V$
118		feq1	$⊢ f = g \cup ((U ∖ dom g) \times \{\emptyset\}) \to (f : U ⟶ J \leftrightarrow (g \cup ((U ∖ dom g) \times \{\emptyset\})) : U ⟶ J)$
119		rneq	$⊢ f = g \cup ((U ∖ dom g) \times \{\emptyset\}) \to ran f = ran (g \cup ((U ∖ dom g) \times \{\emptyset\}))$
120	119	breq1d	$⊢ f = g \cup ((U ∖ dom g) \times \{\emptyset\}) \to (ran f Ref U \leftrightarrow ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) Ref U)$
121	119	eleq1d	$⊢ f = g \cup ((U ∖ dom g) \times \{\emptyset\}) \to (ran f \in LocFin (J) \leftrightarrow ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) \in LocFin (J))$
122	118 120 121	3anbi123d	$⊢ f = g \cup ((U ∖ dom g) \times \{\emptyset\}) \to ((f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J)) \leftrightarrow ((g \cup ((U ∖ dom g) \times \{\emptyset\})) : U ⟶ J \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) Ref U \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) \in LocFin (J)))$
123	122	spcegv	$⊢ g \cup ((U ∖ dom g) \times \{\emptyset\}) \in V \to (((g \cup ((U ∖ dom g) \times \{\emptyset\})) : U ⟶ J \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) Ref U \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) \in LocFin (J)) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J)))$
124	111 114 117 123	4syl	$⊢ (φ \land U \neq \emptyset) \to (((g \cup ((U ∖ dom g) \times \{\emptyset\})) : U ⟶ J \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) Ref U \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) \in LocFin (J)) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J)))$
125	124	imp	$⊢ ((φ \land U \neq \emptyset) \land ((g \cup ((U ∖ dom g) \times \{\emptyset\})) : U ⟶ J \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) Ref U \land ran (g \cup ((U ∖ dom g) \times \{\emptyset\})) \in LocFin (J))) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J))$
126	49 70 93 106 125	syl13anc	$⊢ ((φ \land U \neq \emptyset) \land ((Fun g \land dom g \subseteq U \land ran g \subseteq J) \land (ran g Ref U \land ran g \in LocFin (J)))) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J))$
127	48 126	exlimddv	$⊢ (φ \land U \neq \emptyset) \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J))$
128	46 127	pm2.61dane	$⊢ φ \to \exists f (f : U ⟶ J \land ran f Ref U \land ran f \in LocFin (J))$

Metamath Proof Explorer

Theorem locfinref

Proof