Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  locfinreflem Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 locfinref.4 . . . 4 (𝜑𝑉Ref𝑈)
2 locfinref.5 . . . . 5 (𝜑𝑉 ∈ (LocFin‘𝐽))
3 reff 30716 . . . . 5 (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
42, 3syl 17 . . . 4 (𝜑 → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
51, 4mpbid 233 . . 3 (𝜑 → ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))))
65simprd 496 . 2 (𝜑 → ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))
7 funmpt 6270 . . . . . 6 Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
87a1i 11 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
9 eqid 2797 . . . . . . 7 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
109dmmptss 5977 . . . . . 6 dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ ran 𝑔
11 frn 6395 . . . . . . 7 (𝑔:𝑉𝑈 → ran 𝑔𝑈)
1211ad2antlr 723 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran 𝑔𝑈)
1310, 12sstrid 3906 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈)
14 locfintop 21817 . . . . . . . . . 10 (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
152, 14syl 17 . . . . . . . . 9 (𝜑𝐽 ∈ Top)
1615ad3antrrr 726 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top)
17 cnvimass 5832 . . . . . . . . . 10 (𝑔 “ {𝑢}) ⊆ dom 𝑔
18 fdm 6397 . . . . . . . . . . 11 (𝑔:𝑉𝑈 → dom 𝑔 = 𝑉)
1918ad3antlr 727 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉)
2017, 19sseqtrid 3946 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝑉)
21 locfinref.3 . . . . . . . . . 10 (𝜑𝑉𝐽)
2221ad3antrrr 726 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉𝐽)
2320, 22sstrd 3905 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝐽)
24 uniopn 21193 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝑔 “ {𝑢}) ⊆ 𝐽) → (𝑔 “ {𝑢}) ∈ 𝐽)
2516, 23, 24syl2anc 584 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ∈ 𝐽)
2625ralrimiva 3151 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽)
279rnmptss 6756 . . . . . 6 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
2826, 27syl 17 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
29 eqid 2797 . . . . . . . . . 10 𝑉 = 𝑉
30 eqid 2797 . . . . . . . . . 10 𝑈 = 𝑈
3129, 30refbas 21806 . . . . . . . . 9 (𝑉Ref𝑈 𝑈 = 𝑉)
321, 31syl 17 . . . . . . . 8 (𝜑 𝑈 = 𝑉)
3332ad2antrr 722 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = 𝑉)
34 nfv 1896 . . . . . . . . . . . . 13 𝑣(𝜑𝑔:𝑉𝑈)
35 nfra1 3188 . . . . . . . . . . . . 13 𝑣𝑣𝑉 𝑣 ⊆ (𝑔𝑣)
3634, 35nfan 1885 . . . . . . . . . . . 12 𝑣((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
37 nfre1 3271 . . . . . . . . . . . 12 𝑣𝑣𝑉 𝑥𝑣
3836, 37nfan 1885 . . . . . . . . . . 11 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣)
39 ffn 6389 . . . . . . . . . . . . . . 15 (𝑔:𝑉𝑈𝑔 Fn 𝑉)
4039ad4antlr 729 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
41 simplr 765 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑣𝑉)
42 fnfvelrn 6720 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑉𝑣𝑉) → (𝑔𝑣) ∈ ran 𝑔)
4340, 41, 42syl2anc 584 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → (𝑔𝑣) ∈ ran 𝑔)
44 ssid 3916 . . . . . . . . . . . . . . 15 𝑣𝑣
4539ad3antlr 727 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑔 Fn 𝑉)
46 eqid 2797 . . . . . . . . . . . . . . . . 17 (𝑔𝑣) = (𝑔𝑣)
47 fniniseg 6702 . . . . . . . . . . . . . . . . . 18 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {(𝑔𝑣)}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))))
4847biimpar 478 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn 𝑉 ∧ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
4946, 48mpanr2 700 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝑉𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
5045, 49sylancom 588 . . . . . . . . . . . . . . 15 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
51 ssuni 4773 . . . . . . . . . . . . . . 15 ((𝑣𝑣𝑣 ∈ (𝑔 “ {(𝑔𝑣)})) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5244, 50, 51sylancr 587 . . . . . . . . . . . . . 14 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5352sselda 3895 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑥 (𝑔 “ {(𝑔𝑣)}))
54 sneq 4488 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑔𝑣) → {𝑢} = {(𝑔𝑣)})
5554imaeq2d 5813 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5655unieqd 4761 . . . . . . . . . . . . . . 15 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5756eleq2d 2870 . . . . . . . . . . . . . 14 (𝑢 = (𝑔𝑣) → (𝑥 (𝑔 “ {𝑢}) ↔ 𝑥 (𝑔 “ {(𝑔𝑣)})))
5857rspcev 3561 . . . . . . . . . . . . 13 (((𝑔𝑣) ∈ ran 𝑔𝑥 (𝑔 “ {(𝑔𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
5943, 53, 58syl2anc 584 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
6059adantllr 715 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
61 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑣𝑉 𝑥𝑣)
6238, 60, 61r19.29af 3294 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
63 nfv 1896 . . . . . . . . . . . . . 14 𝑣 𝑢 ∈ ran 𝑔
6436, 63nfan 1885 . . . . . . . . . . . . 13 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔)
65 nfv 1896 . . . . . . . . . . . . 13 𝑣 𝑥 (𝑔 “ {𝑢})
6664, 65nfan 1885 . . . . . . . . . . . 12 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢}))
6720ad3antrrr 726 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → (𝑔 “ {𝑢}) ⊆ 𝑉)
68 simplr 765 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣 ∈ (𝑔 “ {𝑢}))
6967, 68sseldd 3896 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣𝑉)
70 simpr 485 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑥𝑣)
71 simpr 485 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → 𝑥 (𝑔 “ {𝑢}))
72 eluni2 4755 . . . . . . . . . . . . 13 (𝑥 (𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7371, 72sylib 219 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7466, 69, 70, 73reximd2a 3275 . . . . . . . . . . 11 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7574r19.29an 3253 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7662, 75impbida 797 . . . . . . . . 9 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (∃𝑣𝑉 𝑥𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})))
77 eluni2 4755 . . . . . . . . 9 (𝑥 𝑉 ↔ ∃𝑣𝑉 𝑥𝑣)
78 eliun 4835 . . . . . . . . 9 (𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
7976, 77, 783bitr4g 315 . . . . . . . 8 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑥 𝑉𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8079eqrdv 2795 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑉 = 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
81 dfiun3g 5723 . . . . . . . 8 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8226, 81syl 17 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8333, 80, 823eqtrd 2837 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8411ad3antlr 727 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ran 𝑔𝑈)
85 vex 3443 . . . . . . . . . . 11 𝑤 ∈ V
869elrnmpt 5717 . . . . . . . . . . 11 (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8785, 86mp1i 13 . . . . . . . . . 10 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8887biimpa 477 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}))
89 ssrexv 3961 . . . . . . . . 9 (ran 𝑔𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢})))
9084, 88, 89sylc 65 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}))
91 nfv 1896 . . . . . . . . . 10 𝑢((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
92 nfmpt1 5065 . . . . . . . . . . . 12 𝑢(𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9392nfrn 5713 . . . . . . . . . . 11 𝑢ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9493nfcri 2945 . . . . . . . . . 10 𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9591, 94nfan 1885 . . . . . . . . 9 𝑢(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
96 simpr 485 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤 = (𝑔 “ {𝑢}))
97 nfv 1896 . . . . . . . . . . . . . . . 16 𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9836, 97nfan 1885 . . . . . . . . . . . . . . 15 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
99 nfv 1896 . . . . . . . . . . . . . . 15 𝑣 𝑢𝑈
10098, 99nfan 1885 . . . . . . . . . . . . . 14 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈)
101 nfv 1896 . . . . . . . . . . . . . 14 𝑣 𝑤 = (𝑔 “ {𝑢})
102100, 101nfan 1885 . . . . . . . . . . . . 13 𝑣(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢}))
103 simp-5r 782 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
10439ad5antlr 731 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑔 Fn 𝑉)
105 fniniseg 6702 . . . . . . . . . . . . . . . . . . 19 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
106104, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
107106biimpa 477 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢))
108107simpld 495 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑉)
109 rspa 3175 . . . . . . . . . . . . . . . 16 ((∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣) ∧ 𝑣𝑉) → 𝑣 ⊆ (𝑔𝑣))
110103, 108, 109syl2anc 584 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔𝑣))
111107simprd 496 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑔𝑣) = 𝑢)
112110, 111sseqtrd 3934 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑢)
113112ex 413 . . . . . . . . . . . . 13 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) → 𝑣𝑢))
114102, 113ralrimi 3185 . . . . . . . . . . . 12 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
115 unissb 4782 . . . . . . . . . . . 12 ( (𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
116114, 115sylibr 235 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑔 “ {𝑢}) ⊆ 𝑢)
11796, 116eqsstrd 3932 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤𝑢)
118117exp31 420 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (𝑢𝑈 → (𝑤 = (𝑔 “ {𝑢}) → 𝑤𝑢)))
11995, 118reximdai 3274 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤𝑢))
12090, 119mpd 15 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤𝑢)
121120ralrimiva 3151 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))∃𝑢𝑈 𝑤𝑢)
122 vex 3443 . . . . . . . . . 10 𝑔 ∈ V
123122rnex 7480 . . . . . . . . 9 ran 𝑔 ∈ V
124123mptex 6859 . . . . . . . 8 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V
125 rnexg 7477 . . . . . . . 8 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
126124, 125mp1i 13 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
127 eqid 2797 . . . . . . . 8 ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
128127, 30isref 21805 . . . . . . 7 (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V → (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ↔ ( 𝑈 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))∃𝑢𝑈 𝑤𝑢)))
129126, 128syl 17 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ↔ ( 𝑈 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))∃𝑢𝑈 𝑤𝑢)))
13083, 121, 129mpbir2and 709 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈)
13115ad2antrr 722 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝐽 ∈ Top)
132 locfinref.2 . . . . . . . 8 (𝜑𝑋 = 𝑈)
133132ad2antrr 722 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = 𝑈)
134133, 83eqtrd 2833 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
135 nfv 1896 . . . . . . . . 9 𝑣 𝑥𝑋
13636, 135nfan 1885 . . . . . . . 8 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋)
137 simplr 765 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → 𝑣𝐽)
138 ffun 6392 . . . . . . . . . . . . . 14 (𝑔:𝑉𝑈 → Fun 𝑔)
139138ad6antlr 733 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔)
140 imafi 8670 . . . . . . . . . . . . 13 ((Fun 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
141139, 140sylancom 588 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
142 simp3 1131 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘))
143 sneq 4488 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑘 → {𝑢} = {𝑘})
144143imaeq2d 5813 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑘 → (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
145144unieqd 4761 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑘 (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
146122cnvex 7493 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔 ∈ V
147 imaexg 7483 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ V → (𝑔 “ {𝑘}) ∈ V)
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 “ {𝑘}) ∈ V
149148uniex 7330 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 “ {𝑘}) ∈ V
150145, 9, 149fvmpt 6642 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
1511503ad2ant2 1127 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
152142, 151eqtrd 2833 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = (𝑔 “ {𝑘}))
153152ineq1d 4114 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → (𝑤𝑣) = ( (𝑔 “ {𝑘}) ∩ 𝑣))
154153neeq1d 3045 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑤𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅))
155123a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V)
156 imaexg 7483 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ V → (𝑔 “ {𝑢}) ∈ V)
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑔 “ {𝑢}) ∈ V
158157uniex 7330 . . . . . . . . . . . . . . . . . . 19 (𝑔 “ {𝑢}) ∈ V
159158, 9fnmpti 6366 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔
160 dffn4 6471 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
161159, 160mpbi 231 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
162161a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
163154, 155, 162rabfodom 29954 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅})
164 sneq 4488 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑢 → {𝑘} = {𝑢})
165164imaeq2d 5813 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑢 → (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
166165unieqd 4761 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
167166ineq1d 4114 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → ( (𝑔 “ {𝑘}) ∩ 𝑣) = ( (𝑔 “ {𝑢}) ∩ 𝑣))
168167neeq1d 3045 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑢 → (( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅))
169168cbvrabv 3437 . . . . . . . . . . . . . . 15 {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}
170163, 169syl6breq 5009 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅})
171123rabex 5133 . . . . . . . . . . . . . . 15 {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V
172 nfv 1896 . . . . . . . . . . . . . . . . . . . . 21 𝑗(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣)
173 nfrab1 3346 . . . . . . . . . . . . . . . . . . . . . 22 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}
174173nfel1 2965 . . . . . . . . . . . . . . . . . . . . 21 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin
175172, 174nfan 1885 . . . . . . . . . . . . . . . . . . . 20 𝑗((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)
176 nfv 1896 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑢 ∈ ran 𝑔
177175, 176nfan 1885 . . . . . . . . . . . . . . . . . . 19 𝑗(((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔)
178 nfv 1896 . . . . . . . . . . . . . . . . . . 19 𝑗( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅
179177, 178nfan 1885 . . . . . . . . . . . . . . . . . 18 𝑗((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)
180 nfv 1896 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑔𝑘) = 𝑢
181173, 180nfrex 3273 . . . . . . . . . . . . . . . . . 18 𝑗𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢
18239ad5antlr 731 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
183182ad5antr 730 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑔 Fn 𝑉)
184 simplr 765 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ (𝑔 “ {𝑢}))
185 fniniseg 6702 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 Fn 𝑉 → (𝑗 ∈ (𝑔 “ {𝑢}) ↔ (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢)))
186185biimpa 477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 Fn 𝑉𝑗 ∈ (𝑔 “ {𝑢})) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
187183, 184, 186syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
188187simpld 495 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗𝑉)
189 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑣) ≠ ∅)
190 rabid 3339 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ↔ (𝑗𝑉 ∧ (𝑗𝑣) ≠ ∅))
191188, 189, 190sylanbrc 583 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})
192187simprd 496 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑔𝑗) = 𝑢)
193 fveqeq2 6554 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝑔𝑘) = 𝑢 ↔ (𝑔𝑗) = 𝑢))
194193rspcev 3561 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∧ (𝑔𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
195191, 192, 194syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
196 uniinn0 29987 . . . . . . . . . . . . . . . . . . . 20 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
197196biimpi 217 . . . . . . . . . . . . . . . . . . 19 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
198197adantl 482 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
199179, 181, 195, 198r19.29af2 3293 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
200199ex 413 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢))
201200ss2rabdv 3979 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
202 ssdomg 8410 . . . . . . . . . . . . . . 15 ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}))
203171, 201, 202mpsyl 68 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
204 domtr 8417 . . . . . . . . . . . . . 14 (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
205170, 203, 204syl2anc 584 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
206182adantr 481 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉)
207 dffn3 6400 . . . . . . . . . . . . . . 15 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
208207biimpi 217 . . . . . . . . . . . . . 14 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
209 ssrab2 3983 . . . . . . . . . . . . . . 15 {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉
210 fimarab 30076 . . . . . . . . . . . . . . 15 ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
211209, 210mpan2 687 . . . . . . . . . . . . . 14 (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
212206, 208, 2113syl 18 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
213205, 212breqtrrd 4996 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}))
214 domfi 8592 . . . . . . . . . . . 12 (((𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
215141, 213, 214syl2anc 584 . . . . . . . . . . 11 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
216215ex 413 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → ({𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
217216imdistanda 572 . . . . . . . . 9 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) → ((𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
218217imp 407 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
219 simplll 771 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → 𝜑)
220 locfinref.x . . . . . . . . . . . . 13 𝑋 = 𝐽
221220, 29islocfin 21813 . . . . . . . . . . . 12 (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
2222, 221sylib 219 . . . . . . . . . . 11 (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
223222simp3d 1137 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
224223r19.21bi 3177 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
225219, 224sylancom 588 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
226136, 137, 218, 225reximd2a 3275 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
227226ralrimiva 3151 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
228220, 127islocfin 21813 . . . . . 6 (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
229131, 134, 227, 228syl3anbrc 1336 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))
230 funeq 6252 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))))
231 dmeq 5665 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
232231sseq1d 3925 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (dom 𝑓𝑈 ↔ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈))
233 rneq 5695 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
234233sseq1d 3925 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓𝐽 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽))
235230, 232, 2343anbi123d 1428 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)))
236233breq1d 4978 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈))
237233eleq1d 2869 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))
238236, 237anbi12d 630 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))))
239235, 238anbi12d 630 . . . . . 6 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) ↔ ((Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))))
240124, 239spcev 3551 . . . . 5 (((Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
2418, 13, 28, 130, 229, 240syl32anc 1371 . . . 4 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
242241expl 458 . . 3 (𝜑 → ((𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
243242exlimdv 1915 . 2 (𝜑 → (∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
2446, 243mpd 15 1 (𝜑 → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
Colors of variables: wff setvar class
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  ontowfo 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
  Copyright terms: Public domain W3C validator