Theorem locfinreflem 31108

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 31107	. . . . 5 ⊢ (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))))
4	2, 3	syl 17	. . . 4 ⊢ (𝜑 → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))))
5	1, 4	mpbid 234	. . 3 ⊢ (𝜑 → (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))))
6	5	simprd 498	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))
7		funmpt 6396	. . . . . 6 ⊢ Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
8	7	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
9		eqid 2824	. . . . . . 7 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
10	9	dmmptss 6098	. . . . . 6 ⊢ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ ran 𝑔
11		frn 6523	. . . . . . 7 ⊢ (𝑔:𝑉⟶𝑈 → ran 𝑔 ⊆ 𝑈)
12	11	ad2antlr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran 𝑔 ⊆ 𝑈)
13	10, 12	sstrid 3981	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈)
14		locfintop 22132	. . . . . . . . . 10 ⊢ (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
15	2, 14	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ Top)
16	15	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top)
17		cnvimass 5952	. . . . . . . . . 10 ⊢ (◡𝑔 “ {𝑢}) ⊆ dom 𝑔
18		fdm 6525	. . . . . . . . . . 11 ⊢ (𝑔:𝑉⟶𝑈 → dom 𝑔 = 𝑉)
19	18	ad3antlr 729	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉)
20	17, 19	sseqtrid 4022	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝑉)
21		locfinref.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ⊆ 𝐽)
22	21	ad3antrrr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉 ⊆ 𝐽)
23	20, 22	sstrd 3980	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝐽)
24		uniopn 21508	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (◡𝑔 “ {𝑢}) ⊆ 𝐽) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
25	16, 23, 24	syl2anc 586	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
26	25	ralrimiva 3185	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
27	9	rnmptss 6889	. . . . . 6 ⊢ (∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)
28	26, 27	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)
29		eqid 2824	. . . . . . . . . 10 ⊢ ∪ 𝑉 = ∪ 𝑉
30		eqid 2824	. . . . . . . . . 10 ⊢ ∪ 𝑈 = ∪ 𝑈
31	29, 30	refbas 22121	. . . . . . . . 9 ⊢ (𝑉Ref𝑈 → ∪ 𝑈 = ∪ 𝑉)
32	1, 31	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑈 = ∪ 𝑉)
33	32	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪ 𝑉)
34		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑔:𝑉⟶𝑈)
35		nfra1 3222	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)
36	34, 35	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
37		nfre1 3309	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣
38	36, 37	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
39		ffn 6517	. . . . . . . . . . . . . . 15 ⊢ (𝑔:𝑉⟶𝑈 → 𝑔 Fn 𝑉)
40	39	ad4antlr 731	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉)
41		simplr 767	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉)
42		fnfvelrn 6851	. . . . . . . . . . . . . 14 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → (𝑔‘𝑣) ∈ ran 𝑔)
43	40, 41, 42	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → (𝑔‘𝑣) ∈ ran 𝑔)
44		ssid 3992	. . . . . . . . . . . . . . 15 ⊢ 𝑣 ⊆ 𝑣
45	39	ad3antlr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑔 Fn 𝑉)
46		eqid 2824	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑣) = (𝑔‘𝑣)
47		fniniseg 6833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣))))
48	47	biimpar 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn 𝑉 ∧ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣))) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
49	46, 48	mpanr2 702	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
50	45, 49	sylancom 590	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
51		ssuni 4866	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ 𝑣 ∧ 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)})) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
52	44, 50, 51	sylancr 589	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
53	52	sselda 3970	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
54		sneq 4580	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑔‘𝑣) → {𝑢} = {(𝑔‘𝑣)})
55	54	imaeq2d 5932	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑔‘𝑣) → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {(𝑔‘𝑣)}))
56	55	unieqd 4855	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑔‘𝑣) → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
57	56	eleq2d 2901	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑔‘𝑣) → (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})))
58	57	rspcev 3626	. . . . . . . . . . . . 13 ⊢ (((𝑔‘𝑣) ∈ ran 𝑔 ∧ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
59	43, 53, 58	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
60	59	adantllr 717	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
61		simpr 487	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
62	38, 60, 61	r19.29af 3334	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
63		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣 𝑢 ∈ ran 𝑔
64	36, 63	nfan 1899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔)
65		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})
66	64, 65	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
67	20	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → (◡𝑔 “ {𝑢}) ⊆ 𝑉)
68		simplr 767	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ (◡𝑔 “ {𝑢}))
69	67, 68	sseldd 3971	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉)
70		simpr 487	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣)
71		simpr 487	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
72		eluni2 4845	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣)
73	71, 72	sylib 220	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣)
74	66, 69, 70, 73	reximd2a 3315	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
75	74	r19.29an 3291	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
76	62, 75	impbida 799	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})))
77		eluni2 4845	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑉 ↔ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
78		eliun 4926	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
79	76, 77, 78	3bitr4g 316	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑥 ∈ ∪ 𝑉 ↔ 𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢})))
80	79	eqrdv 2822	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑉 = ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}))
81		dfiun3g 5838	. . . . . . . 8 ⊢ (∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
82	26, 81	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
83	33, 80, 82	3eqtrd 2863	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
84	11	ad3antlr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ran 𝑔 ⊆ 𝑈)
85		vex 3500	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
86	9	elrnmpt 5831	. . . . . . . . . . 11 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢})))
87	85, 86	mp1i 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢})))
88	87	biimpa 479	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}))
89		ssrexv 4037	. . . . . . . . 9 ⊢ (ran 𝑔 ⊆ 𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢})))
90	84, 88, 89	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}))
91		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑢((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
92		nfmpt1 5167	. . . . . . . . . . . 12 ⊢ Ⅎ𝑢(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
93	92	nfrn 5827	. . . . . . . . . . 11 ⊢ Ⅎ𝑢ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
94	93	nfcri 2974	. . . . . . . . . 10 ⊢ Ⅎ𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
95	91, 94	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑢(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
96		simpr 487	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 = ∪ (◡𝑔 “ {𝑢}))
97		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
98	36, 97	nfan 1899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
99		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑣 𝑢 ∈ 𝑈
100	98, 99	nfan 1899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈)
101		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣 𝑤 = ∪ (◡𝑔 “ {𝑢})
102	100, 101	nfan 1899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢}))
103		simp-5r 784	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
104	39	ad5antlr 733	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑔 Fn 𝑉)
105		fniniseg 6833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢)))
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢)))
107	106	biimpa 479	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢))
108	107	simpld 497	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ∈ 𝑉)
109		rspa 3209	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ (𝑔‘𝑣))
110	103, 108, 109	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔‘𝑣))
111	107	simprd 498	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑔‘𝑣) = 𝑢)
112	110, 111	sseqtrd 4010	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ 𝑢)
113	112	ex 415	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) → 𝑣 ⊆ 𝑢))
114	102, 113	ralrimi 3219	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢)
115		unissb 4873	. . . . . . . . . . . 12 ⊢ (∪ (◡𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢)
116	114, 115	sylibr 236	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∪ (◡𝑔 “ {𝑢}) ⊆ 𝑢)
117	96, 116	eqsstrd 4008	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 ⊆ 𝑢)
118	117	exp31 422	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (𝑢 ∈ 𝑈 → (𝑤 = ∪ (◡𝑔 “ {𝑢}) → 𝑤 ⊆ 𝑢)))
119	95, 118	reximdai 3314	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢))
120	90, 119	mpd 15	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)
121	120	ralrimiva 3185	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)
122		vex 3500	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
123	122	rnex 7620	. . . . . . . . 9 ⊢ ran 𝑔 ∈ V
124	123	mptex 6989	. . . . . . . 8 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V
125		rnexg 7617	. . . . . . . 8 ⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V)
126	124, 125	mp1i 13	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V)
127		eqid 2824	. . . . . . . 8 ⊢ ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
128	127, 30	isref 22120	. . . . . . 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 2859	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
135		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑣 𝑥 ∈ 𝑋
136	36, 135	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋)
137		simplr 767	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → 𝑣 ∈ 𝐽)
138		ffun 6520	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝑉⟶𝑈 → Fun 𝑔)
139	138	ad6antlr 735	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔)
140		imafi 8820	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin)
141	139, 140	sylancom 590	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin)
142		simp3 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘))
143		sneq 4580	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑘 → {𝑢} = {𝑘})
144	143	imaeq2d 5932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑘 → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {𝑘}))
145	144	unieqd 4855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑘 → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {𝑘}))
146	122	cnvex 7633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ◡𝑔 ∈ V
147		imaexg 7623	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑘}) ∈ V)
148	146, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡𝑔 “ {𝑘}) ∈ V
149	148	uniex 7470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ (◡𝑔 “ {𝑘}) ∈ V
150	145, 9, 149	fvmpt 6771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘}))
151	150	3ad2ant2 1130	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘}))
152	142, 151	eqtrd 2859	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ∪ (◡𝑔 “ {𝑘}))
153	152	ineq1d 4191	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → (𝑤 ∩ 𝑣) = (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣))
154	153	neeq1d 3078	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑤 ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅))
155	123	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V)
156		imaexg 7623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑢}) ∈ V)
157	146, 156	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡𝑔 “ {𝑢}) ∈ V
158	157	uniex 7470	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (◡𝑔 “ {𝑢}) ∈ V
159	158, 9	fnmpti 6494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔
160		dffn4 6599	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
161	159, 160	mpbi 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
162	161	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
163	154, 155, 162	rabfodom 30269	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅})
164		sneq 4580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑢 → {𝑘} = {𝑢})
165	164	imaeq2d 5932	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑢 → (◡𝑔 “ {𝑘}) = (◡𝑔 “ {𝑢}))
166	165	unieqd 4855	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → ∪ (◡𝑔 “ {𝑘}) = ∪ (◡𝑔 “ {𝑢}))
167	166	ineq1d 4191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) = (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣))
168	167	neeq1d 3078	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑢 → ((∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅))
169	168	cbvrabv 3494	. . . . . . . . . . . . . . 15 ⊢ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}
170	163, 169	breqtrdi 5110	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅})
171	123	rabex 5238	. . . . . . . . . . . . . . 15 ⊢ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V
172		nfv 1914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑗(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣)
173		nfrab1 3387	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}
174	173	nfel1 2997	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin
175	172, 174	nfan 1899	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)
176		nfv 1914	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗 𝑢 ∈ ran 𝑔
177	175, 176	nfan 1899	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔)
178		nfv 1914	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅
179	177, 178	nfan 1899	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)
180		nfv 1914	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(𝑔‘𝑘) = 𝑢
181	173, 180	nfrex 3312	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢
182	39	ad5antlr 733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉)
183	182	ad5antr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑔 Fn 𝑉)
184		simplr 767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ (◡𝑔 “ {𝑢}))
185		fniniseg 6833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 Fn 𝑉 → (𝑗 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢)))
186	185	biimpa 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢))
187	183, 184, 186	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢))
188	187	simpld 497	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ 𝑉)
189		simpr 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∩ 𝑣) ≠ ∅)
190		rabid 3381	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ↔ (𝑗 ∈ 𝑉 ∧ (𝑗 ∩ 𝑣) ≠ ∅))
191	188, 189, 190	sylanbrc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})
192	187	simprd 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑔‘𝑗) = 𝑢)
193		fveqeq2 6682	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) = 𝑢 ↔ (𝑔‘𝑗) = 𝑢))
194	193	rspcev 3626	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∧ (𝑔‘𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
195	191, 192, 194	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
196		uniinn0 30305	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
197	196	biimpi 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
198	197	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
199	179, 181, 195, 198	r19.29af2 3333	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
200	199	ex 415	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢))
201	200	ss2rabdv 4055	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
202		ssdomg 8558	. . . . . . . . . . . . . . 15 ⊢ ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}))
203	171, 201, 202	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
204		domtr 8565	. . . . . . . . . . . . . 14 ⊢ (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
205	170, 203, 204	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
206	182	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉)
207		dffn3 6528	. . . . . . . . . . . . . . 15 ⊢ (𝑔 Fn 𝑉 ↔ 𝑔:𝑉⟶ran 𝑔)
208	207	biimpi 218	. . . . . . . . . . . . . 14 ⊢ (𝑔 Fn 𝑉 → 𝑔:𝑉⟶ran 𝑔)
209		ssrab2 4059	. . . . . . . . . . . . . . 15 ⊢ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉
210		fimarab 30393	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
211	209, 210	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
212	206, 208, 211	3syl 18	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
213	205, 212	breqtrrd 5097	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}))
214		domfi 8742	. . . . . . . . . . . 12 ⊢ (((𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)
215	141, 213, 214	syl2anc 586	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)
216	215	ex 415	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → ({𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
217	216	imdistanda 574	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) → ((𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)))
218	217	imp 409	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
219		simplll 773	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → 𝜑)
220		locfinref.x	. . . . . . . . . . . . 13 ⊢ 𝑋 = ∪ 𝐽
221	220, 29	islocfin 22128	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)))
222	2, 221	sylib 220	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)))
223	222	simp3d 1140	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
224	223	r19.21bi 3211	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
225	219, 224	sylancom 590	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
226	136, 137, 218, 225	reximd2a 3315	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
227	226	ralrimiva 3185	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
228	220, 127	islocfin 22128	. . . . . 6 ⊢ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)))
229	131, 134, 227, 228	syl3anbrc 1339	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))
230		funeq 6378	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))))
231		dmeq 5775	. . . . . . . . 9 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
232	231	sseq1d 4001	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (dom 𝑓 ⊆ 𝑈 ↔ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈))
233		rneq 5809	. . . . . . . . 9 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
234	233	sseq1d 4001	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓 ⊆ 𝐽 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽))
235	230, 232, 234	3anbi123d 1432	. . . . . . 7 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)))
236	233	breq1d 5079	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈))
237	233	eleq1d 2900	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))
238	236, 237	anbi12d 632	. . . . . . 7 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ((ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))))
239	235, 238	anbi12d 632	. . . . . 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 3610	. . . . 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 1374	. . . 4 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
242	241	expl 460	. . 3 ⊢ (𝜑 → ((𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
243	242	exlimdv 1933	. 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 208   ∧ wa 398   ∧ w3a 1083   = wceq 1536  ∃wex 1779   ∈ wcel 2113   ≠ wne 3019  ∀wral 3141  ∃wrex 3142  {crab 3145  Vcvv 3497   ∩ cin 3938   ⊆ wss 3939  ∅c0 4294  {csn 4570  ∪ cuni 4841  ∪ ciun 4922   class class class wbr 5069   ↦ cmpt 5149  ^◡ccnv 5557  dom cdm 5558  ran crn 5559   “ cima 5561  Fun wfun 6352   Fn wfn 6353  ⟶wf 6354  –onto→wfo 6356  ‘cfv 6358   ≼ cdom 8510  Fincfn 8512  Topctop 21504  Refcref 22113  LocFinclocfin 22115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-reg 9059  ax-inf2 9107  ax-ac2 9888

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-int 4880  df-iun 4924  df-iin 4925  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-se 5518  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-isom 6367  df-riota 7117  df-om 7584  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-er 8292  df-en 8513  df-dom 8514  df-fin 8516  df-r1 9196  df-rank 9197  df-card 9371  df-ac 9545  df-top 21505  df-ref 22116  df-locfin 22118

This theorem is referenced by:  locfinref  31109