Theorem locfinreflem 33655

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 𝑓 from the original cover 𝑈, 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.)

Hypotheses

Ref	Expression
locfinref.x	⊢ 𝑋 = ∪ 𝐽
locfinref.1	⊢ (𝜑 → 𝑈 ⊆ 𝐽)
locfinref.2	⊢ (𝜑 → 𝑋 = ∪ 𝑈)
locfinref.3	⊢ (𝜑 → 𝑉 ⊆ 𝐽)
locfinref.4	⊢ (𝜑 → 𝑉Ref𝑈)
locfinref.5	⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽))

Assertion

Ref	Expression
locfinreflem	⊢ (𝜑 → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))

Distinct variable groups:   𝑓,𝐽   𝑈,𝑓   𝑓,𝑉   𝜑,𝑓

Allowed substitution hint:   𝑋(𝑓)

Proof of Theorem locfinreflem

Dummy variables 𝑔 𝑗 𝑘 𝑢 𝑣 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		locfinref.4	. . . 4 ⊢ (𝜑 → 𝑉Ref𝑈)
2		locfinref.5	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽))
3		reff 33654	. . . . 5 ⊢ (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))))
4	2, 3	syl 17	. . . 4 ⊢ (𝜑 → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))))
5	1, 4	mpbid 231	. . 3 ⊢ (𝜑 → (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))))
6	5	simprd 494	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))
7		funmpt 6597	. . . . . 6 ⊢ Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
8	7	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
9		eqid 2726	. . . . . . 7 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
10	9	dmmptss 6252	. . . . . 6 ⊢ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ ran 𝑔
11		frn 6735	. . . . . . 7 ⊢ (𝑔:𝑉⟶𝑈 → ran 𝑔 ⊆ 𝑈)
12	11	ad2antlr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran 𝑔 ⊆ 𝑈)
13	10, 12	sstrid 3991	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈)
14		locfintop 23516	. . . . . . . . . 10 ⊢ (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
15	2, 14	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ Top)
16	15	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top)
17		cnvimass 6091	. . . . . . . . . 10 ⊢ (◡𝑔 “ {𝑢}) ⊆ dom 𝑔
18		fdm 6737	. . . . . . . . . . 11 ⊢ (𝑔:𝑉⟶𝑈 → dom 𝑔 = 𝑉)
19	18	ad3antlr 729	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉)
20	17, 19	sseqtrid 4032	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝑉)
21		locfinref.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ⊆ 𝐽)
22	21	ad3antrrr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉 ⊆ 𝐽)
23	20, 22	sstrd 3990	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝐽)
24		uniopn 22890	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (◡𝑔 “ {𝑢}) ⊆ 𝐽) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
25	16, 23, 24	syl2anc 582	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
26	25	ralrimiva 3136	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
27	9	rnmptss 7137	. . . . . 6 ⊢ (∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)
28	26, 27	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)
29		eqid 2726	. . . . . . . . . 10 ⊢ ∪ 𝑉 = ∪ 𝑉
30		eqid 2726	. . . . . . . . . 10 ⊢ ∪ 𝑈 = ∪ 𝑈
31	29, 30	refbas 23505	. . . . . . . . 9 ⊢ (𝑉Ref𝑈 → ∪ 𝑈 = ∪ 𝑉)
32	1, 31	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑈 = ∪ 𝑉)
33	32	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪ 𝑉)
34		nfv 1910	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑔:𝑉⟶𝑈)
35		nfra1 3272	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)
36	34, 35	nfan 1895	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
37		nfre1 3273	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣
38	36, 37	nfan 1895	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
39		ffn 6728	. . . . . . . . . . . . . . 15 ⊢ (𝑔:𝑉⟶𝑈 → 𝑔 Fn 𝑉)
40	39	ad4antlr 731	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉)
41		simplr 767	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉)
42		fnfvelrn 7094	. . . . . . . . . . . . . 14 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → (𝑔‘𝑣) ∈ ran 𝑔)
43	40, 41, 42	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → (𝑔‘𝑣) ∈ ran 𝑔)
44		ssid 4002	. . . . . . . . . . . . . . 15 ⊢ 𝑣 ⊆ 𝑣
45	39	ad3antlr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑔 Fn 𝑉)
46		eqid 2726	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑣) = (𝑔‘𝑣)
47		fniniseg 7073	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣))))
48	47	biimpar 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn 𝑉 ∧ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣))) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
49	46, 48	mpanr2 702	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
50	45, 49	sylancom 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
51		ssuni 4940	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ 𝑣 ∧ 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)})) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
52	44, 50, 51	sylancr 585	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
53	52	sselda 3979	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
54		sneq 4643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑔‘𝑣) → {𝑢} = {(𝑔‘𝑣)})
55	54	imaeq2d 6069	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑔‘𝑣) → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {(𝑔‘𝑣)}))
56	55	unieqd 4926	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑔‘𝑣) → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
57	56	eleq2d 2812	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑔‘𝑣) → (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})))
58	57	rspcev 3608	. . . . . . . . . . . . 13 ⊢ (((𝑔‘𝑣) ∈ ran 𝑔 ∧ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
59	43, 53, 58	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
60	59	adantllr 717	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
61		simpr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
62	38, 60, 61	r19.29af 3256	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
63		nfv 1910	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣 𝑢 ∈ ran 𝑔
64	36, 63	nfan 1895	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔)
65		nfv 1910	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})
66	64, 65	nfan 1895	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
67	20	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → (◡𝑔 “ {𝑢}) ⊆ 𝑉)
68		simplr 767	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ (◡𝑔 “ {𝑢}))
69	67, 68	sseldd 3980	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉)
70		simpr 483	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣)
71		simpr 483	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
72		eluni2 4917	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣)
73	71, 72	sylib 217	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣)
74	66, 69, 70, 73	reximd2a 3257	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
75	74	r19.29an 3148	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
76	62, 75	impbida 799	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})))
77		eluni2 4917	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑉 ↔ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
78		eliun 5005	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
79	76, 77, 78	3bitr4g 313	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑥 ∈ ∪ 𝑉 ↔ 𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢})))
80	79	eqrdv 2724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑉 = ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}))
81		dfiun3g 5971	. . . . . . . 8 ⊢ (∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
82	26, 81	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
83	33, 80, 82	3eqtrd 2770	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
84	11	ad3antlr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ran 𝑔 ⊆ 𝑈)
85		vex 3466	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
86	9	elrnmpt 5962	. . . . . . . . . . 11 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢})))
87	85, 86	mp1i 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢})))
88	87	biimpa 475	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}))
89		ssrexv 4049	. . . . . . . . 9 ⊢ (ran 𝑔 ⊆ 𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢})))
90	84, 88, 89	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}))
91		nfv 1910	. . . . . . . . . 10 ⊢ Ⅎ𝑢((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
92		nfmpt1 5261	. . . . . . . . . . . 12 ⊢ Ⅎ𝑢(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
93	92	nfrn 5958	. . . . . . . . . . 11 ⊢ Ⅎ𝑢ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
94	93	nfcri 2883	. . . . . . . . . 10 ⊢ Ⅎ𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
95	91, 94	nfan 1895	. . . . . . . . 9 ⊢ Ⅎ𝑢(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
96		simpr 483	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 = ∪ (◡𝑔 “ {𝑢}))
97		nfv 1910	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
98	36, 97	nfan 1895	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
99		nfv 1910	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑣 𝑢 ∈ 𝑈
100	98, 99	nfan 1895	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈)
101		nfv 1910	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣 𝑤 = ∪ (◡𝑔 “ {𝑢})
102	100, 101	nfan 1895	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢}))
103		simp-5r 784	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
104	39	ad5antlr 733	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑔 Fn 𝑉)
105		fniniseg 7073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢)))
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢)))
107	106	biimpa 475	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢))
108	107	simpld 493	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ∈ 𝑉)
109		rspa 3236	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ (𝑔‘𝑣))
110	103, 108, 109	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔‘𝑣))
111	107	simprd 494	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑔‘𝑣) = 𝑢)
112	110, 111	sseqtrd 4020	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ 𝑢)
113	112	ex 411	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) → 𝑣 ⊆ 𝑢))
114	102, 113	ralrimi 3245	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢)
115		unissb 4947	. . . . . . . . . . . 12 ⊢ (∪ (◡𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢)
116	114, 115	sylibr 233	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∪ (◡𝑔 “ {𝑢}) ⊆ 𝑢)
117	96, 116	eqsstrd 4018	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 ⊆ 𝑢)
118	117	exp31 418	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (𝑢 ∈ 𝑈 → (𝑤 = ∪ (◡𝑔 “ {𝑢}) → 𝑤 ⊆ 𝑢)))
119	95, 118	reximdai 3249	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢))
120	90, 119	mpd 15	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)
121	120	ralrimiva 3136	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)
122		vex 3466	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
123	122	rnex 7923	. . . . . . . . 9 ⊢ ran 𝑔 ∈ V
124	123	mptex 7240	. . . . . . . 8 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V
125		rnexg 7915	. . . . . . . 8 ⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V)
126	124, 125	mp1i 13	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V)
127		eqid 2726	. . . . . . . 8 ⊢ ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
128	127, 30	isref 23504	. . . . . . 7 ⊢ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V → (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ↔ (∪ 𝑈 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)))
129	126, 128	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ↔ (∪ 𝑈 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)))
130	83, 121, 129	mpbir2and 711	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈)
131	15	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝐽 ∈ Top)
132		locfinref.2	. . . . . . . 8 ⊢ (𝜑 → 𝑋 = ∪ 𝑈)
133	132	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝑋 = ∪ 𝑈)
134	133, 83	eqtrd 2766	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
135		nfv 1910	. . . . . . . . 9 ⊢ Ⅎ𝑣 𝑥 ∈ 𝑋
136	36, 135	nfan 1895	. . . . . . . 8 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋)
137		simplr 767	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → 𝑣 ∈ 𝐽)
138		ffun 6731	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝑉⟶𝑈 → Fun 𝑔)
139	138	ad6antlr 735	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔)
140		imafi 9355	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin)
141	139, 140	sylancom 586	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin)
142		simp3 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘))
143		sneq 4643	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑘 → {𝑢} = {𝑘})
144	143	imaeq2d 6069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑘 → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {𝑘}))
145	144	unieqd 4926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑘 → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {𝑘}))
146	122	cnvex 7938	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ◡𝑔 ∈ V
147		imaexg 7926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑘}) ∈ V)
148	146, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡𝑔 “ {𝑘}) ∈ V
149	148	uniex 7752	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ (◡𝑔 “ {𝑘}) ∈ V
150	145, 9, 149	fvmpt 7009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘}))
151	150	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘}))
152	142, 151	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ∪ (◡𝑔 “ {𝑘}))
153	152	ineq1d 4212	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → (𝑤 ∩ 𝑣) = (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣))
154	153	neeq1d 2990	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑤 ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅))
155	123	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V)
156		imaexg 7926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑢}) ∈ V)
157	146, 156	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡𝑔 “ {𝑢}) ∈ V
158	157	uniex 7752	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (◡𝑔 “ {𝑢}) ∈ V
159	158, 9	fnmpti 6704	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔
160		dffn4 6821	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
161	159, 160	mpbi 229	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
162	161	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
163	154, 155, 162	rabfodom 32431	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅})
164		sneq 4643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑢 → {𝑘} = {𝑢})
165	164	imaeq2d 6069	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑢 → (◡𝑔 “ {𝑘}) = (◡𝑔 “ {𝑢}))
166	165	unieqd 4926	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → ∪ (◡𝑔 “ {𝑘}) = ∪ (◡𝑔 “ {𝑢}))
167	166	ineq1d 4212	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) = (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣))
168	167	neeq1d 2990	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑢 → ((∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅))
169	168	cbvrabv 3430	. . . . . . . . . . . . . . 15 ⊢ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}
170	163, 169	breqtrdi 5194	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅})
171	123	rabex 5339	. . . . . . . . . . . . . . 15 ⊢ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V
172		nfv 1910	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑗(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣)
173		nfrab1 3439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}
174	173	nfel1 2909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin
175	172, 174	nfan 1895	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)
176		nfv 1910	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗 𝑢 ∈ ran 𝑔
177	175, 176	nfan 1895	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔)
178		nfv 1910	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅
179	177, 178	nfan 1895	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)
180		nfv 1910	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(𝑔‘𝑘) = 𝑢
181	173, 180	nfrexw 3301	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢
182	39	ad5antlr 733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉)
183	182	ad5antr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑔 Fn 𝑉)
184		simplr 767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ (◡𝑔 “ {𝑢}))
185		fniniseg 7073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 Fn 𝑉 → (𝑗 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢)))
186	185	biimpa 475	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢))
187	183, 184, 186	syl2anc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢))
188	187	simpld 493	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ 𝑉)
189		simpr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∩ 𝑣) ≠ ∅)
190		rabid 3440	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ↔ (𝑗 ∈ 𝑉 ∧ (𝑗 ∩ 𝑣) ≠ ∅))
191	188, 189, 190	sylanbrc 581	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})
192	187	simprd 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑔‘𝑗) = 𝑢)
193		fveqeq2 6910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) = 𝑢 ↔ (𝑔‘𝑗) = 𝑢))
194	193	rspcev 3608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∧ (𝑔‘𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
195	191, 192, 194	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
196		uniinn0 32471	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
197	196	biimpi 215	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
198	197	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
199	179, 181, 195, 198	r19.29af2 3255	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
200	199	ex 411	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢))
201	200	ss2rabdv 4072	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
202		ssdomg 9031	. . . . . . . . . . . . . . 15 ⊢ ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}))
203	171, 201, 202	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
204		domtr 9038	. . . . . . . . . . . . . 14 ⊢ (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
205	170, 203, 204	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
206	182	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉)
207		dffn3 6740	. . . . . . . . . . . . . . 15 ⊢ (𝑔 Fn 𝑉 ↔ 𝑔:𝑉⟶ran 𝑔)
208	207	biimpi 215	. . . . . . . . . . . . . 14 ⊢ (𝑔 Fn 𝑉 → 𝑔:𝑉⟶ran 𝑔)
209		ssrab2 4076	. . . . . . . . . . . . . . 15 ⊢ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉
210		fimarab 32560	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
211	209, 210	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
212	206, 208, 211	3syl 18	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
213	205, 212	breqtrrd 5181	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}))
214		domfi 9226	. . . . . . . . . . . 12 ⊢ (((𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)
215	141, 213, 214	syl2anc 582	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)
216	215	ex 411	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → ({𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
217	216	imdistanda 570	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) → ((𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)))
218	217	imp 405	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
219		simplll 773	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → 𝜑)
220		locfinref.x	. . . . . . . . . . . . 13 ⊢ 𝑋 = ∪ 𝐽
221	220, 29	islocfin 23512	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)))
222	2, 221	sylib 217	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)))
223	222	simp3d 1141	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
224	223	r19.21bi 3239	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
225	219, 224	sylancom 586	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
226	136, 137, 218, 225	reximd2a 3257	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
227	226	ralrimiva 3136	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
228	220, 127	islocfin 23512	. . . . . 6 ⊢ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)))
229	131, 134, 227, 228	syl3anbrc 1340	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))
230		funeq 6579	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))))
231		dmeq 5910	. . . . . . . . 9 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
232	231	sseq1d 4011	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (dom 𝑓 ⊆ 𝑈 ↔ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈))
233		rneq 5942	. . . . . . . . 9 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
234	233	sseq1d 4011	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓 ⊆ 𝐽 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽))
235	230, 232, 234	3anbi123d 1433	. . . . . . 7 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)))
236	233	breq1d 5163	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈))
237	233	eleq1d 2811	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))
238	236, 237	anbi12d 630	. . . . . . 7 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ((ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))))
239	235, 238	anbi12d 630	. . . . . 6 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) ↔ ((Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))))
240	124, 239	spcev 3592	. . . . 5 ⊢ (((Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
241	8, 13, 28, 130, 229, 240	syl32anc 1375	. . . 4 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
242	241	expl 456	. . 3 ⊢ (𝜑 → ((𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
243	242	exlimdv 1929	. 2 ⊢ (𝜑 → (∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
244	6, 243	mpd 15	1 ⊢ (𝜑 → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1534  ∃wex 1774   ∈ wcel 2099   ≠ wne 2930  ∀wral 3051  ∃wrex 3060  {crab 3419  Vcvv 3462   ∩ cin 3946   ⊆ wss 3947  ∅c0 4325  {csn 4633  ∪ cuni 4913  ∪ ciun 5001   class class class wbr 5153   ↦ cmpt 5236  ^◡ccnv 5681  dom cdm 5682  ran crn 5683   “ cima 5685  Fun wfun 6548   Fn wfn 6549  ⟶wf 6550  –onto→wfo 6552  ‘cfv 6554   ≼ cdom 8972  Fincfn 8974  Topctop 22886  Refcref 23497  LocFinclocfin 23499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-reg 9635  ax-inf2 9684  ax-ac2 10506

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-iin 5004  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-om 7877  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-er 8734  df-en 8975  df-dom 8976  df-fin 8978  df-r1 9807  df-rank 9808  df-card 9982  df-ac 10159  df-top 22887  df-ref 23500  df-locfin 23502

This theorem is referenced by:  locfinref  33656