Theorem locfinreflem 33800

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 33799	. . . . 5 ⊢ (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))))
4	2, 3	syl 17	. . . 4 ⊢ (𝜑 → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))))
5	1, 4	mpbid 232	. . 3 ⊢ (𝜑 → (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))))
6	5	simprd 495	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))
7		funmpt 6605	. . . . . 6 ⊢ Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
8	7	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
9		eqid 2734	. . . . . . 7 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
10	9	dmmptss 6262	. . . . . 6 ⊢ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ ran 𝑔
11		frn 6743	. . . . . . 7 ⊢ (𝑔:𝑉⟶𝑈 → ran 𝑔 ⊆ 𝑈)
12	11	ad2antlr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran 𝑔 ⊆ 𝑈)
13	10, 12	sstrid 4006	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈)
14		locfintop 23544	. . . . . . . . . 10 ⊢ (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
15	2, 14	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ Top)
16	15	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top)
17		cnvimass 6101	. . . . . . . . . 10 ⊢ (◡𝑔 “ {𝑢}) ⊆ dom 𝑔
18		fdm 6745	. . . . . . . . . . 11 ⊢ (𝑔:𝑉⟶𝑈 → dom 𝑔 = 𝑉)
19	18	ad3antlr 731	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉)
20	17, 19	sseqtrid 4047	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝑉)
21		locfinref.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ⊆ 𝐽)
22	21	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉 ⊆ 𝐽)
23	20, 22	sstrd 4005	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝐽)
24		uniopn 22918	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (◡𝑔 “ {𝑢}) ⊆ 𝐽) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
25	16, 23, 24	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
26	25	ralrimiva 3143	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
27	9	rnmptss 7142	. . . . . 6 ⊢ (∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)
28	26, 27	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)
29		eqid 2734	. . . . . . . . . 10 ⊢ ∪ 𝑉 = ∪ 𝑉
30		eqid 2734	. . . . . . . . . 10 ⊢ ∪ 𝑈 = ∪ 𝑈
31	29, 30	refbas 23533	. . . . . . . . 9 ⊢ (𝑉Ref𝑈 → ∪ 𝑈 = ∪ 𝑉)
32	1, 31	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑈 = ∪ 𝑉)
33	32	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪ 𝑉)
34		nfv 1911	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑔:𝑉⟶𝑈)
35		nfra1 3281	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)
36	34, 35	nfan 1896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
37		nfre1 3282	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣
38	36, 37	nfan 1896	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
39		ffn 6736	. . . . . . . . . . . . . . 15 ⊢ (𝑔:𝑉⟶𝑈 → 𝑔 Fn 𝑉)
40	39	ad4antlr 733	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉)
41		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉)
42		fnfvelrn 7099	. . . . . . . . . . . . . 14 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → (𝑔‘𝑣) ∈ ran 𝑔)
43	40, 41, 42	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → (𝑔‘𝑣) ∈ ran 𝑔)
44		ssid 4017	. . . . . . . . . . . . . . 15 ⊢ 𝑣 ⊆ 𝑣
45	39	ad3antlr 731	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑔 Fn 𝑉)
46		eqid 2734	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑣) = (𝑔‘𝑣)
47		fniniseg 7079	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣))))
48	47	biimpar 477	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn 𝑉 ∧ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣))) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
49	46, 48	mpanr2 704	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
50	45, 49	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
51		ssuni 4936	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ 𝑣 ∧ 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)})) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
52	44, 50, 51	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
53	52	sselda 3994	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
54		sneq 4640	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑔‘𝑣) → {𝑢} = {(𝑔‘𝑣)})
55	54	imaeq2d 6079	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑔‘𝑣) → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {(𝑔‘𝑣)}))
56	55	unieqd 4924	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑔‘𝑣) → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
57	56	eleq2d 2824	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑔‘𝑣) → (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})))
58	57	rspcev 3621	. . . . . . . . . . . . 13 ⊢ (((𝑔‘𝑣) ∈ ran 𝑔 ∧ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
59	43, 53, 58	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
60	59	adantllr 719	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
61		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
62	38, 60, 61	r19.29af 3265	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
63		nfv 1911	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣 𝑢 ∈ ran 𝑔
64	36, 63	nfan 1896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔)
65		nfv 1911	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})
66	64, 65	nfan 1896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
67	20	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → (◡𝑔 “ {𝑢}) ⊆ 𝑉)
68		simplr 769	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ (◡𝑔 “ {𝑢}))
69	67, 68	sseldd 3995	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉)
70		simpr 484	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣)
71		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
72		eluni2 4915	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣)
73	71, 72	sylib 218	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣)
74	66, 69, 70, 73	reximd2a 3266	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
75	74	r19.29an 3155	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
76	62, 75	impbida 801	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})))
77		eluni2 4915	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑉 ↔ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
78		eliun 4999	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
79	76, 77, 78	3bitr4g 314	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑥 ∈ ∪ 𝑉 ↔ 𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢})))
80	79	eqrdv 2732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑉 = ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}))
81		dfiun3g 5980	. . . . . . . 8 ⊢ (∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
82	26, 81	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
83	33, 80, 82	3eqtrd 2778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
84	11	ad3antlr 731	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ran 𝑔 ⊆ 𝑈)
85		vex 3481	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
86	9	elrnmpt 5971	. . . . . . . . . . 11 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢})))
87	85, 86	mp1i 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢})))
88	87	biimpa 476	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}))
89		ssrexv 4064	. . . . . . . . 9 ⊢ (ran 𝑔 ⊆ 𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢})))
90	84, 88, 89	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}))
91		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑢((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
92		nfmpt1 5255	. . . . . . . . . . . 12 ⊢ Ⅎ𝑢(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
93	92	nfrn 5965	. . . . . . . . . . 11 ⊢ Ⅎ𝑢ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
94	93	nfcri 2894	. . . . . . . . . 10 ⊢ Ⅎ𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
95	91, 94	nfan 1896	. . . . . . . . 9 ⊢ Ⅎ𝑢(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
96		simpr 484	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 = ∪ (◡𝑔 “ {𝑢}))
97		nfv 1911	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
98	36, 97	nfan 1896	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
99		nfv 1911	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑣 𝑢 ∈ 𝑈
100	98, 99	nfan 1896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈)
101		nfv 1911	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣 𝑤 = ∪ (◡𝑔 “ {𝑢})
102	100, 101	nfan 1896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢}))
103		simp-5r 786	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
104	39	ad5antlr 735	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑔 Fn 𝑉)
105		fniniseg 7079	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢)))
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢)))
107	106	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢))
108	107	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ∈ 𝑉)
109		rspa 3245	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ (𝑔‘𝑣))
110	103, 108, 109	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔‘𝑣))
111	107	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑔‘𝑣) = 𝑢)
112	110, 111	sseqtrd 4035	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ 𝑢)
113	112	ex 412	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) → 𝑣 ⊆ 𝑢))
114	102, 113	ralrimi 3254	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢)
115		unissb 4943	. . . . . . . . . . . 12 ⊢ (∪ (◡𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢)
116	114, 115	sylibr 234	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∪ (◡𝑔 “ {𝑢}) ⊆ 𝑢)
117	96, 116	eqsstrd 4033	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 ⊆ 𝑢)
118	117	exp31 419	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (𝑢 ∈ 𝑈 → (𝑤 = ∪ (◡𝑔 “ {𝑢}) → 𝑤 ⊆ 𝑢)))
119	95, 118	reximdai 3258	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢))
120	90, 119	mpd 15	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)
121	120	ralrimiva 3143	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)
122		vex 3481	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
123	122	rnex 7932	. . . . . . . . 9 ⊢ ran 𝑔 ∈ V
124	123	mptex 7242	. . . . . . . 8 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V
125		rnexg 7924	. . . . . . . 8 ⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V)
126	124, 125	mp1i 13	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V)
127		eqid 2734	. . . . . . . 8 ⊢ ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
128	127, 30	isref 23532	. . . . . . 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 713	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈)
131	15	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝐽 ∈ Top)
132		locfinref.2	. . . . . . . 8 ⊢ (𝜑 → 𝑋 = ∪ 𝑈)
133	132	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝑋 = ∪ 𝑈)
134	133, 83	eqtrd 2774	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
135		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑣 𝑥 ∈ 𝑋
136	36, 135	nfan 1896	. . . . . . . 8 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋)
137		simplr 769	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → 𝑣 ∈ 𝐽)
138		ffun 6739	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝑉⟶𝑈 → Fun 𝑔)
139	138	ad6antlr 737	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔)
140		imafi 9350	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin)
141	139, 140	sylancom 588	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin)
142		simp3 1137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘))
143		sneq 4640	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑘 → {𝑢} = {𝑘})
144	143	imaeq2d 6079	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑘 → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {𝑘}))
145	144	unieqd 4924	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑘 → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {𝑘}))
146	122	cnvex 7947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ◡𝑔 ∈ V
147		imaexg 7935	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑘}) ∈ V)
148	146, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡𝑔 “ {𝑘}) ∈ V
149	148	uniex 7759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ (◡𝑔 “ {𝑘}) ∈ V
150	145, 9, 149	fvmpt 7015	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘}))
151	150	3ad2ant2 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘}))
152	142, 151	eqtrd 2774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ∪ (◡𝑔 “ {𝑘}))
153	152	ineq1d 4226	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → (𝑤 ∩ 𝑣) = (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣))
154	153	neeq1d 2997	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑤 ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅))
155	123	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V)
156		imaexg 7935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑢}) ∈ V)
157	146, 156	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡𝑔 “ {𝑢}) ∈ V
158	157	uniex 7759	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (◡𝑔 “ {𝑢}) ∈ V
159	158, 9	fnmpti 6711	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔
160		dffn4 6826	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
161	159, 160	mpbi 230	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
162	161	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
163	154, 155, 162	rabfodom 32532	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅})
164		sneq 4640	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑢 → {𝑘} = {𝑢})
165	164	imaeq2d 6079	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑢 → (◡𝑔 “ {𝑘}) = (◡𝑔 “ {𝑢}))
166	165	unieqd 4924	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → ∪ (◡𝑔 “ {𝑘}) = ∪ (◡𝑔 “ {𝑢}))
167	166	ineq1d 4226	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) = (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣))
168	167	neeq1d 2997	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑢 → ((∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅))
169	168	cbvrabv 3443	. . . . . . . . . . . . . . 15 ⊢ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}
170	163, 169	breqtrdi 5188	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅})
171	123	rabex 5344	. . . . . . . . . . . . . . 15 ⊢ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V
172		nfv 1911	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑗(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣)
173		nfrab1 3453	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}
174	173	nfel1 2919	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin
175	172, 174	nfan 1896	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)
176		nfv 1911	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗 𝑢 ∈ ran 𝑔
177	175, 176	nfan 1896	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔)
178		nfv 1911	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅
179	177, 178	nfan 1896	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)
180		nfv 1911	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(𝑔‘𝑘) = 𝑢
181	173, 180	nfrexw 3310	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢
182	39	ad5antlr 735	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉)
183	182	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑔 Fn 𝑉)
184		simplr 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ (◡𝑔 “ {𝑢}))
185		fniniseg 7079	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 Fn 𝑉 → (𝑗 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢)))
186	185	biimpa 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢))
187	183, 184, 186	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢))
188	187	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ 𝑉)
189		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∩ 𝑣) ≠ ∅)
190		rabid 3454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ↔ (𝑗 ∈ 𝑉 ∧ (𝑗 ∩ 𝑣) ≠ ∅))
191	188, 189, 190	sylanbrc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})
192	187	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑔‘𝑗) = 𝑢)
193		fveqeq2 6915	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) = 𝑢 ↔ (𝑔‘𝑗) = 𝑢))
194	193	rspcev 3621	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∧ (𝑔‘𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
195	191, 192, 194	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
196		uniinn0 32570	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
197	196	biimpi 216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
198	197	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
199	179, 181, 195, 198	r19.29af2 3264	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
200	199	ex 412	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢))
201	200	ss2rabdv 4085	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
202		ssdomg 9038	. . . . . . . . . . . . . . 15 ⊢ ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}))
203	171, 201, 202	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
204		domtr 9045	. . . . . . . . . . . . . 14 ⊢ (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
205	170, 203, 204	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
206	182	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉)
207		dffn3 6748	. . . . . . . . . . . . . . 15 ⊢ (𝑔 Fn 𝑉 ↔ 𝑔:𝑉⟶ran 𝑔)
208	207	biimpi 216	. . . . . . . . . . . . . 14 ⊢ (𝑔 Fn 𝑉 → 𝑔:𝑉⟶ran 𝑔)
209		ssrab2 4089	. . . . . . . . . . . . . . 15 ⊢ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉
210		fimarab 6982	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
211	209, 210	mpan2 691	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
212	206, 208, 211	3syl 18	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
213	205, 212	breqtrrd 5175	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}))
214		domfi 9226	. . . . . . . . . . . 12 ⊢ (((𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)
215	141, 213, 214	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)
216	215	ex 412	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → ({𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
217	216	imdistanda 571	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) → ((𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)))
218	217	imp 406	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
219		simplll 775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → 𝜑)
220		locfinref.x	. . . . . . . . . . . . 13 ⊢ 𝑋 = ∪ 𝐽
221	220, 29	islocfin 23540	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)))
222	2, 221	sylib 218	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)))
223	222	simp3d 1143	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
224	223	r19.21bi 3248	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
225	219, 224	sylancom 588	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
226	136, 137, 218, 225	reximd2a 3266	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
227	226	ralrimiva 3143	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
228	220, 127	islocfin 23540	. . . . . 6 ⊢ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)))
229	131, 134, 227, 228	syl3anbrc 1342	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))
230		funeq 6587	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))))
231		dmeq 5916	. . . . . . . . 9 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
232	231	sseq1d 4026	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (dom 𝑓 ⊆ 𝑈 ↔ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈))
233		rneq 5949	. . . . . . . . 9 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
234	233	sseq1d 4026	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓 ⊆ 𝐽 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽))
235	230, 232, 234	3anbi123d 1435	. . . . . . 7 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)))
236	233	breq1d 5157	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈))
237	233	eleq1d 2823	. . . . . . . 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 3605	. . . . 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 1377	. . . 4 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
242	241	expl 457	. . 3 ⊢ (𝜑 → ((𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
243	242	exlimdv 1930	. 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 206   ∧ wa 395   ∧ w3a 1086   = wceq 1536  ∃wex 1775   ∈ wcel 2105   ≠ wne 2937  ∀wral 3058  ∃wrex 3067  {crab 3432  Vcvv 3477   ∩ cin 3961   ⊆ wss 3962  ∅c0 4338  {csn 4630  ∪ cuni 4911  ∪ ciun 4995   class class class wbr 5147   ↦ cmpt 5230  ^◡ccnv 5687  dom cdm 5688  ran crn 5689   “ cima 5691  Fun wfun 6556   Fn wfn 6557  ⟶wf 6558  –onto→wfo 6560  ‘cfv 6562   ≼ cdom 8981  Fincfn 8983  Topctop 22914  Refcref 23525  LocFinclocfin 23527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-reg 9629  ax-inf2 9678  ax-ac2 10500

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-en 8984  df-dom 8985  df-fin 8987  df-r1 9801  df-rank 9802  df-card 9976  df-ac 10153  df-top 22915  df-ref 23528  df-locfin 23530

This theorem is referenced by:  locfinref  33801