Theorem locfinreflem 30717

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 30716	. . . . 5 ⊢ (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))))
4	2, 3	syl 17	. . . 4 ⊢ (𝜑 → (𝑉Ref𝑈 ↔ (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))))
5	1, 4	mpbid 233	. . 3 ⊢ (𝜑 → (∪ 𝑈 ⊆ ∪ 𝑉 ∧ ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))))
6	5	simprd 496	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)))
7		funmpt 6270	. . . . . 6 ⊢ Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
8	7	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
9		eqid 2797	. . . . . . 7 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
10	9	dmmptss 5977	. . . . . 6 ⊢ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ ran 𝑔
11		frn 6395	. . . . . . 7 ⊢ (𝑔:𝑉⟶𝑈 → ran 𝑔 ⊆ 𝑈)
12	11	ad2antlr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran 𝑔 ⊆ 𝑈)
13	10, 12	sstrid 3906	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈)
14		locfintop 21817	. . . . . . . . . 10 ⊢ (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
15	2, 14	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ Top)
16	15	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top)
17		cnvimass 5832	. . . . . . . . . 10 ⊢ (◡𝑔 “ {𝑢}) ⊆ dom 𝑔
18		fdm 6397	. . . . . . . . . . 11 ⊢ (𝑔:𝑉⟶𝑈 → dom 𝑔 = 𝑉)
19	18	ad3antlr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉)
20	17, 19	sseqtrid 3946	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝑉)
21		locfinref.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ⊆ 𝐽)
22	21	ad3antrrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉 ⊆ 𝐽)
23	20, 22	sstrd 3905	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (◡𝑔 “ {𝑢}) ⊆ 𝐽)
24		uniopn 21193	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (◡𝑔 “ {𝑢}) ⊆ 𝐽) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
25	16, 23, 24	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) → ∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
26	25	ralrimiva 3151	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽)
27	9	rnmptss 6756	. . . . . 6 ⊢ (∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)
28	26, 27	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)
29		eqid 2797	. . . . . . . . . 10 ⊢ ∪ 𝑉 = ∪ 𝑉
30		eqid 2797	. . . . . . . . . 10 ⊢ ∪ 𝑈 = ∪ 𝑈
31	29, 30	refbas 21806	. . . . . . . . 9 ⊢ (𝑉Ref𝑈 → ∪ 𝑈 = ∪ 𝑉)
32	1, 31	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑈 = ∪ 𝑉)
33	32	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪ 𝑉)
34		nfv 1896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑔:𝑉⟶𝑈)
35		nfra1 3188	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)
36	34, 35	nfan 1885	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
37		nfre1 3271	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣
38	36, 37	nfan 1885	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
39		ffn 6389	. . . . . . . . . . . . . . 15 ⊢ (𝑔:𝑉⟶𝑈 → 𝑔 Fn 𝑉)
40	39	ad4antlr 729	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉)
41		simplr 765	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉)
42		fnfvelrn 6720	. . . . . . . . . . . . . 14 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → (𝑔‘𝑣) ∈ ran 𝑔)
43	40, 41, 42	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → (𝑔‘𝑣) ∈ ran 𝑔)
44		ssid 3916	. . . . . . . . . . . . . . 15 ⊢ 𝑣 ⊆ 𝑣
45	39	ad3antlr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑔 Fn 𝑉)
46		eqid 2797	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔‘𝑣) = (𝑔‘𝑣)
47		fniniseg 6702	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣))))
48	47	biimpar 478	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn 𝑉 ∧ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = (𝑔‘𝑣))) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
49	46, 48	mpanr2 700	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
50	45, 49	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)}))
51		ssuni 4773	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ⊆ 𝑣 ∧ 𝑣 ∈ (◡𝑔 “ {(𝑔‘𝑣)})) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
52	44, 50, 51	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
53	52	sselda 3895	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
54		sneq 4488	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑔‘𝑣) → {𝑢} = {(𝑔‘𝑣)})
55	54	imaeq2d 5813	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑔‘𝑣) → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {(𝑔‘𝑣)}))
56	55	unieqd 4761	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑔‘𝑣) → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {(𝑔‘𝑣)}))
57	56	eleq2d 2870	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑔‘𝑣) → (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})))
58	57	rspcev 3561	. . . . . . . . . . . . 13 ⊢ (((𝑔‘𝑣) ∈ ran 𝑔 ∧ 𝑥 ∈ ∪ (◡𝑔 “ {(𝑔‘𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
59	43, 53, 58	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
60	59	adantllr 715	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) ∧ 𝑣 ∈ 𝑉) ∧ 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
61		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
62	38, 60, 61	r19.29af 3294	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
63		nfv 1896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣 𝑢 ∈ ran 𝑔
64	36, 63	nfan 1885	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔)
65		nfv 1896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})
66	64, 65	nfan 1885	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
67	20	ad3antrrr 726	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → (◡𝑔 “ {𝑢}) ⊆ 𝑉)
68		simplr 765	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ (◡𝑔 “ {𝑢}))
69	67, 68	sseldd 3896	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑣 ∈ 𝑉)
70		simpr 485	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) ∧ 𝑥 ∈ 𝑣) → 𝑥 ∈ 𝑣)
71		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
72		eluni2 4755	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣)
73	71, 72	sylib 219	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ (◡𝑔 “ {𝑢})𝑥 ∈ 𝑣)
74	66, 69, 70, 73	reximd2a 3275	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
75	74	r19.29an 3253	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})) → ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
76	62, 75	impbida 797	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢})))
77		eluni2 4755	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑉 ↔ ∃𝑣 ∈ 𝑉 𝑥 ∈ 𝑣)
78		eliun 4835	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 ∈ ∪ (◡𝑔 “ {𝑢}))
79	76, 77, 78	3bitr4g 315	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑥 ∈ ∪ 𝑉 ↔ 𝑥 ∈ ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢})))
80	79	eqrdv 2795	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑉 = ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}))
81		dfiun3g 5723	. . . . . . . 8 ⊢ (∀𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) ∈ 𝐽 → ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
82	26, 81	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑢 ∈ ran 𝑔∪ (◡𝑔 “ {𝑢}) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
83	33, 80, 82	3eqtrd 2837	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∪ 𝑈 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
84	11	ad3antlr 727	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ran 𝑔 ⊆ 𝑈)
85		vex 3443	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
86	9	elrnmpt 5717	. . . . . . . . . . 11 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢})))
87	85, 86	mp1i 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢})))
88	87	biimpa 477	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}))
89		ssrexv 3961	. . . . . . . . 9 ⊢ (ran 𝑔 ⊆ 𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢})))
90	84, 88, 89	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}))
91		nfv 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑢((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
92		nfmpt1 5065	. . . . . . . . . . . 12 ⊢ Ⅎ𝑢(𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
93	92	nfrn 5713	. . . . . . . . . . 11 ⊢ Ⅎ𝑢ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
94	93	nfcri 2945	. . . . . . . . . 10 ⊢ Ⅎ𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
95	91, 94	nfan 1885	. . . . . . . . 9 ⊢ Ⅎ𝑢(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
96		simpr 485	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 = ∪ (◡𝑔 “ {𝑢}))
97		nfv 1896	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
98	36, 97	nfan 1885	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
99		nfv 1896	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑣 𝑢 ∈ 𝑈
100	98, 99	nfan 1885	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈)
101		nfv 1896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣 𝑤 = ∪ (◡𝑔 “ {𝑢})
102	100, 101	nfan 1885	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢}))
103		simp-5r 782	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣))
104	39	ad5antlr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑔 Fn 𝑉)
105		fniniseg 6702	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 Fn 𝑉 → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢)))
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢)))
107	106	biimpa 477	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑣 ∈ 𝑉 ∧ (𝑔‘𝑣) = 𝑢))
108	107	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ∈ 𝑉)
109		rspa 3175	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣) ∧ 𝑣 ∈ 𝑉) → 𝑣 ⊆ (𝑔‘𝑣))
110	103, 108, 109	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔‘𝑣))
111	107	simprd 496	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → (𝑔‘𝑣) = 𝑢)
112	110, 111	sseqtrd 3934	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) ∧ 𝑣 ∈ (◡𝑔 “ {𝑢})) → 𝑣 ⊆ 𝑢)
113	112	ex 413	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → (𝑣 ∈ (◡𝑔 “ {𝑢}) → 𝑣 ⊆ 𝑢))
114	102, 113	ralrimi 3185	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢)
115		unissb 4782	. . . . . . . . . . . 12 ⊢ (∪ (◡𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (◡𝑔 “ {𝑢})𝑣 ⊆ 𝑢)
116	114, 115	sylibr 235	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → ∪ (◡𝑔 “ {𝑢}) ⊆ 𝑢)
117	96, 116	eqsstrd 3932	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 = ∪ (◡𝑔 “ {𝑢})) → 𝑤 ⊆ 𝑢)
118	117	exp31 420	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (𝑢 ∈ 𝑈 → (𝑤 = ∪ (◡𝑔 “ {𝑢}) → 𝑤 ⊆ 𝑢)))
119	95, 118	reximdai 3274	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → (∃𝑢 ∈ 𝑈 𝑤 = ∪ (◡𝑔 “ {𝑢}) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢))
120	90, 119	mpd 15	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))) → ∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)
121	120	ralrimiva 3151	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))∃𝑢 ∈ 𝑈 𝑤 ⊆ 𝑢)
122		vex 3443	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
123	122	rnex 7480	. . . . . . . . 9 ⊢ ran 𝑔 ∈ V
124	123	mptex 6859	. . . . . . . 8 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V
125		rnexg 7477	. . . . . . . 8 ⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V)
126	124, 125	mp1i 13	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ V)
127		eqid 2797	. . . . . . . 8 ⊢ ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
128	127, 30	isref 21805	. . . . . . 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 709	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈)
131	15	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝐽 ∈ Top)
132		locfinref.2	. . . . . . . 8 ⊢ (𝜑 → 𝑋 = ∪ 𝑈)
133	132	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝑋 = ∪ 𝑈)
134	133, 83	eqtrd 2833	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
135		nfv 1896	. . . . . . . . 9 ⊢ Ⅎ𝑣 𝑥 ∈ 𝑋
136	36, 135	nfan 1885	. . . . . . . 8 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋)
137		simplr 765	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → 𝑣 ∈ 𝐽)
138		ffun 6392	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝑉⟶𝑈 → Fun 𝑔)
139	138	ad6antlr 733	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔)
140		imafi 8670	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin)
141	139, 140	sylancom 588	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin)
142		simp3 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘))
143		sneq 4488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = 𝑘 → {𝑢} = {𝑘})
144	143	imaeq2d 5813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 = 𝑘 → (◡𝑔 “ {𝑢}) = (◡𝑔 “ {𝑘}))
145	144	unieqd 4761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 = 𝑘 → ∪ (◡𝑔 “ {𝑢}) = ∪ (◡𝑔 “ {𝑘}))
146	122	cnvex 7493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ◡𝑔 ∈ V
147		imaexg 7483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑘}) ∈ V)
148	146, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡𝑔 “ {𝑘}) ∈ V
149	148	uniex 7330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ (◡𝑔 “ {𝑘}) ∈ V
150	145, 9, 149	fvmpt 6642	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘}))
151	150	3ad2ant2 1127	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘) = ∪ (◡𝑔 “ {𝑘}))
152	142, 151	eqtrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ∪ (◡𝑔 “ {𝑘}))
153	152	ineq1d 4114	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → (𝑤 ∩ 𝑣) = (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣))
154	153	neeq1d 3045	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔 ∧ 𝑤 = ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))‘𝑘)) → ((𝑤 ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅))
155	123	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V)
156		imaexg 7483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡𝑔 ∈ V → (◡𝑔 “ {𝑢}) ∈ V)
157	146, 156	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡𝑔 “ {𝑢}) ∈ V
158	157	uniex 7330	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ (◡𝑔 “ {𝑢}) ∈ V
159	158, 9	fnmpti 6366	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔
160		dffn4 6471	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
161	159, 160	mpbi 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))
162	161	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})):ran 𝑔–onto→ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
163	154, 155, 162	rabfodom 29954	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅})
164		sneq 4488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑢 → {𝑘} = {𝑢})
165	164	imaeq2d 5813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑢 → (◡𝑔 “ {𝑘}) = (◡𝑔 “ {𝑢}))
166	165	unieqd 4761	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑢 → ∪ (◡𝑔 “ {𝑘}) = ∪ (◡𝑔 “ {𝑢}))
167	166	ineq1d 4114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑢 → (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) = (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣))
168	167	neeq1d 3045	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑢 → ((∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅))
169	168	cbvrabv 3437	. . . . . . . . . . . . . . 15 ⊢ {𝑘 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}
170	163, 169	syl6breq 5009	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅})
171	123	rabex 5133	. . . . . . . . . . . . . . 15 ⊢ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V
172		nfv 1896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑗(((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣)
173		nfrab1 3346	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}
174	173	nfel1 2965	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑗{𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin
175	172, 174	nfan 1885	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)
176		nfv 1896	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗 𝑢 ∈ ran 𝑔
177	175, 176	nfan 1885	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔)
178		nfv 1896	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅
179	177, 178	nfan 1885	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)
180		nfv 1896	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(𝑔‘𝑘) = 𝑢
181	173, 180	nfrex 3273	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢
182	39	ad5antlr 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → 𝑔 Fn 𝑉)
183	182	ad5antr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑔 Fn 𝑉)
184		simplr 765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ (◡𝑔 “ {𝑢}))
185		fniniseg 6702	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 Fn 𝑉 → (𝑗 ∈ (◡𝑔 “ {𝑢}) ↔ (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢)))
186	185	biimpa 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 Fn 𝑉 ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢))
187	183, 184, 186	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∈ 𝑉 ∧ (𝑔‘𝑗) = 𝑢))
188	187	simpld 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ 𝑉)
189		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑗 ∩ 𝑣) ≠ ∅)
190		rabid 3339	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ↔ (𝑗 ∈ 𝑉 ∧ (𝑗 ∩ 𝑣) ≠ ∅))
191	188, 189, 190	sylanbrc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → 𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})
192	187	simprd 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → (𝑔‘𝑗) = 𝑢)
193		fveqeq2 6554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑗 → ((𝑔‘𝑘) = 𝑢 ↔ (𝑔‘𝑗) = 𝑢))
194	193	rspcev 3561	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∧ (𝑔‘𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
195	191, 192, 194	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (◡𝑔 “ {𝑢})) ∧ (𝑗 ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
196		uniinn0 29987	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
197	196	biimpi 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
198	197	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (◡𝑔 “ {𝑢})(𝑗 ∩ 𝑣) ≠ ∅)
199	179, 181, 195, 198	r19.29af2 3293	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢)
200	199	ex 413	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → ((∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢))
201	200	ss2rabdv 3979	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
202		ssdomg 8410	. . . . . . . . . . . . . . 15 ⊢ ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}))
203	171, 201, 202	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
204		domtr 8417	. . . . . . . . . . . . . 14 ⊢ (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ (∪ (◡𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
205	170, 203, 204	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
206	182	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉)
207		dffn3 6400	. . . . . . . . . . . . . . 15 ⊢ (𝑔 Fn 𝑉 ↔ 𝑔:𝑉⟶ran 𝑔)
208	207	biimpi 217	. . . . . . . . . . . . . 14 ⊢ (𝑔 Fn 𝑉 → 𝑔:𝑉⟶ran 𝑔)
209		ssrab2 3983	. . . . . . . . . . . . . . 15 ⊢ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉
210		fimarab 30076	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
211	209, 210	mpan2 687	. . . . . . . . . . . . . 14 ⊢ (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
212	206, 208, 211	3syl 18	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} (𝑔‘𝑘) = 𝑢})
213	205, 212	breqtrrd 4996	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}))
214		domfi 8592	. . . . . . . . . . . 12 ⊢ (((𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)
215	141, 213, 214	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)
216	215	ex 413	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ 𝑥 ∈ 𝑣) → ({𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
217	216	imdistanda 572	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) → ((𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)))
218	217	imp 407	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)) → (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
219		simplll 771	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → 𝜑)
220		locfinref.x	. . . . . . . . . . . . 13 ⊢ 𝑋 = ∪ 𝐽
221	220, 29	islocfin 21813	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)))
222	2, 221	sylib 219	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑉 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin)))
223	222	simp3d 1137	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
224	223	r19.21bi 3177	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
225	219, 224	sylancom 588	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑗 ∈ 𝑉 ∣ (𝑗 ∩ 𝑣) ≠ ∅} ∈ Fin))
226	136, 137, 218, 225	reximd2a 3275	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) ∧ 𝑥 ∈ 𝑋) → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
227	226	ralrimiva 3151	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin))
228	220, 127	islocfin 21813	. . . . . 6 ⊢ (ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∣ (𝑤 ∩ 𝑣) ≠ ∅} ∈ Fin)))
229	131, 134, 227, 228	syl3anbrc 1336	. . . . 5 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))
230		funeq 6252	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))))
231		dmeq 5665	. . . . . . . . 9 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
232	231	sseq1d 3925	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (dom 𝑓 ⊆ 𝑈 ↔ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈))
233		rneq 5695	. . . . . . . . 9 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})))
234	233	sseq1d 3925	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓 ⊆ 𝐽 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽))
235	230, 232, 234	3anbi123d 1428	. . . . . . 7 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) ⊆ 𝐽)))
236	233	breq1d 4978	. . . . . . . 8 ⊢ (𝑓 = (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 ↦ ∪ (◡𝑔 “ {𝑢}))Ref𝑈))
237	233	eleq1d 2869	. . . . . . . 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 3551	. . . . 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 1371	. . . 4 ⊢ (((𝜑 ∧ 𝑔:𝑉⟶𝑈) ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
242	241	expl 458	. . 3 ⊢ (𝜑 → ((𝑔:𝑉⟶𝑈 ∧ ∀𝑣 ∈ 𝑉 𝑣 ⊆ (𝑔‘𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
243	242	exlimdv 1915	. 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 207   ∧ wa 396   ∧ w3a 1080   = wceq 1525  ∃wex 1765   ∈ wcel 2083   ≠ wne 2986  ∀wral 3107  ∃wrex 3108  {crab 3111  Vcvv 3440   ∩ cin 3864   ⊆ wss 3865  ∅c0 4217  {csn 4478  ∪ cuni 4751  ∪ ciun 4831   class class class wbr 4968   ↦ cmpt 5047  ^◡ccnv 5449  dom cdm 5450  ran crn 5451   “ cima 5453  Fun wfun 6226   Fn wfn 6227  ⟶wf 6228  –onto→wfo 6230  ‘cfv 6232   ≼ cdom 8362  Fincfn 8364  Topctop 21189  Refcref 21798  LocFinclocfin 21800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-reg 8909  ax-inf2 8957  ax-ac2 9738

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-om 7444  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-er 8146  df-en 8365  df-dom 8366  df-fin 8368  df-r1 9046  df-rank 9047  df-card 9221  df-ac 9395  df-top 21190  df-ref 21801  df-locfin 21803

This theorem is referenced by:  locfinref  30718