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 31197
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 31196 . . . . 5 (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
42, 3syl 17 . . . 4 (𝜑 → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
51, 4mpbid 235 . . 3 (𝜑 → ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))))
65simprd 499 . 2 (𝜑 → ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))
7 funmpt 6366 . . . . . 6 Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
87a1i 11 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
9 eqid 2801 . . . . . . 7 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
109dmmptss 6066 . . . . . 6 dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ ran 𝑔
11 frn 6497 . . . . . . 7 (𝑔:𝑉𝑈 → ran 𝑔𝑈)
1211ad2antlr 726 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran 𝑔𝑈)
1310, 12sstrid 3929 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈)
14 locfintop 22130 . . . . . . . . . 10 (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
152, 14syl 17 . . . . . . . . 9 (𝜑𝐽 ∈ Top)
1615ad3antrrr 729 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top)
17 cnvimass 5920 . . . . . . . . . 10 (𝑔 “ {𝑢}) ⊆ dom 𝑔
18 fdm 6499 . . . . . . . . . . 11 (𝑔:𝑉𝑈 → dom 𝑔 = 𝑉)
1918ad3antlr 730 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉)
2017, 19sseqtrid 3970 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝑉)
21 locfinref.3 . . . . . . . . . 10 (𝜑𝑉𝐽)
2221ad3antrrr 729 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉𝐽)
2320, 22sstrd 3928 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝐽)
24 uniopn 21506 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝑔 “ {𝑢}) ⊆ 𝐽) → (𝑔 “ {𝑢}) ∈ 𝐽)
2516, 23, 24syl2anc 587 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ∈ 𝐽)
2625ralrimiva 3152 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽)
279rnmptss 6867 . . . . . 6 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
2826, 27syl 17 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
29 eqid 2801 . . . . . . . . . 10 𝑉 = 𝑉
30 eqid 2801 . . . . . . . . . 10 𝑈 = 𝑈
3129, 30refbas 22119 . . . . . . . . 9 (𝑉Ref𝑈 𝑈 = 𝑉)
321, 31syl 17 . . . . . . . 8 (𝜑 𝑈 = 𝑉)
3332ad2antrr 725 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = 𝑉)
34 nfv 1915 . . . . . . . . . . . . 13 𝑣(𝜑𝑔:𝑉𝑈)
35 nfra1 3186 . . . . . . . . . . . . 13 𝑣𝑣𝑉 𝑣 ⊆ (𝑔𝑣)
3634, 35nfan 1900 . . . . . . . . . . . 12 𝑣((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
37 nfre1 3268 . . . . . . . . . . . 12 𝑣𝑣𝑉 𝑥𝑣
3836, 37nfan 1900 . . . . . . . . . . 11 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣)
39 ffn 6491 . . . . . . . . . . . . . . 15 (𝑔:𝑉𝑈𝑔 Fn 𝑉)
4039ad4antlr 732 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
41 simplr 768 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑣𝑉)
42 fnfvelrn 6829 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑉𝑣𝑉) → (𝑔𝑣) ∈ ran 𝑔)
4340, 41, 42syl2anc 587 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → (𝑔𝑣) ∈ ran 𝑔)
44 ssid 3940 . . . . . . . . . . . . . . 15 𝑣𝑣
4539ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑔 Fn 𝑉)
46 eqid 2801 . . . . . . . . . . . . . . . . 17 (𝑔𝑣) = (𝑔𝑣)
47 fniniseg 6811 . . . . . . . . . . . . . . . . . 18 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {(𝑔𝑣)}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))))
4847biimpar 481 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn 𝑉 ∧ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
4946, 48mpanr2 703 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝑉𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
5045, 49sylancom 591 . . . . . . . . . . . . . . 15 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
51 ssuni 4828 . . . . . . . . . . . . . . 15 ((𝑣𝑣𝑣 ∈ (𝑔 “ {(𝑔𝑣)})) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5244, 50, 51sylancr 590 . . . . . . . . . . . . . 14 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5352sselda 3918 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑥 (𝑔 “ {(𝑔𝑣)}))
54 sneq 4538 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑔𝑣) → {𝑢} = {(𝑔𝑣)})
5554imaeq2d 5900 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5655unieqd 4817 . . . . . . . . . . . . . . 15 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5756eleq2d 2878 . . . . . . . . . . . . . 14 (𝑢 = (𝑔𝑣) → (𝑥 (𝑔 “ {𝑢}) ↔ 𝑥 (𝑔 “ {(𝑔𝑣)})))
5857rspcev 3574 . . . . . . . . . . . . 13 (((𝑔𝑣) ∈ ran 𝑔𝑥 (𝑔 “ {(𝑔𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
5943, 53, 58syl2anc 587 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
6059adantllr 718 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
61 simpr 488 . . . . . . . . . . 11 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑣𝑉 𝑥𝑣)
6238, 60, 61r19.29af 3292 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
63 nfv 1915 . . . . . . . . . . . . . 14 𝑣 𝑢 ∈ ran 𝑔
6436, 63nfan 1900 . . . . . . . . . . . . 13 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔)
65 nfv 1915 . . . . . . . . . . . . 13 𝑣 𝑥 (𝑔 “ {𝑢})
6664, 65nfan 1900 . . . . . . . . . . . 12 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢}))
6720ad3antrrr 729 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → (𝑔 “ {𝑢}) ⊆ 𝑉)
68 simplr 768 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣 ∈ (𝑔 “ {𝑢}))
6967, 68sseldd 3919 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣𝑉)
70 simpr 488 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑥𝑣)
71 simpr 488 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → 𝑥 (𝑔 “ {𝑢}))
72 eluni2 4807 . . . . . . . . . . . . 13 (𝑥 (𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7371, 72sylib 221 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7466, 69, 70, 73reximd2a 3274 . . . . . . . . . . 11 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7574r19.29an 3250 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7662, 75impbida 800 . . . . . . . . 9 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (∃𝑣𝑉 𝑥𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})))
77 eluni2 4807 . . . . . . . . 9 (𝑥 𝑉 ↔ ∃𝑣𝑉 𝑥𝑣)
78 eliun 4888 . . . . . . . . 9 (𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
7976, 77, 783bitr4g 317 . . . . . . . 8 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑥 𝑉𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8079eqrdv 2799 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑉 = 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
81 dfiun3g 5804 . . . . . . . 8 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8226, 81syl 17 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8333, 80, 823eqtrd 2840 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8411ad3antlr 730 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ran 𝑔𝑈)
85 vex 3447 . . . . . . . . . . 11 𝑤 ∈ V
869elrnmpt 5796 . . . . . . . . . . 11 (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8785, 86mp1i 13 . . . . . . . . . 10 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8887biimpa 480 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}))
89 ssrexv 3985 . . . . . . . . 9 (ran 𝑔𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢})))
9084, 88, 89sylc 65 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}))
91 nfv 1915 . . . . . . . . . 10 𝑢((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
92 nfmpt1 5131 . . . . . . . . . . . 12 𝑢(𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9392nfrn 5792 . . . . . . . . . . 11 𝑢ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9493nfcri 2946 . . . . . . . . . 10 𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9591, 94nfan 1900 . . . . . . . . 9 𝑢(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
96 simpr 488 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤 = (𝑔 “ {𝑢}))
97 nfv 1915 . . . . . . . . . . . . . . . 16 𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9836, 97nfan 1900 . . . . . . . . . . . . . . 15 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
99 nfv 1915 . . . . . . . . . . . . . . 15 𝑣 𝑢𝑈
10098, 99nfan 1900 . . . . . . . . . . . . . 14 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈)
101 nfv 1915 . . . . . . . . . . . . . 14 𝑣 𝑤 = (𝑔 “ {𝑢})
102100, 101nfan 1900 . . . . . . . . . . . . 13 𝑣(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢}))
103 simp-5r 785 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
10439ad5antlr 734 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑔 Fn 𝑉)
105 fniniseg 6811 . . . . . . . . . . . . . . . . . . 19 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
106104, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
107106biimpa 480 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢))
108107simpld 498 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑉)
109 rspa 3174 . . . . . . . . . . . . . . . 16 ((∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣) ∧ 𝑣𝑉) → 𝑣 ⊆ (𝑔𝑣))
110103, 108, 109syl2anc 587 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔𝑣))
111107simprd 499 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑔𝑣) = 𝑢)
112110, 111sseqtrd 3958 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑢)
113112ex 416 . . . . . . . . . . . . 13 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) → 𝑣𝑢))
114102, 113ralrimi 3183 . . . . . . . . . . . 12 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
115 unissb 4835 . . . . . . . . . . . 12 ( (𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
116114, 115sylibr 237 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑔 “ {𝑢}) ⊆ 𝑢)
11796, 116eqsstrd 3956 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤𝑢)
118117exp31 423 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (𝑢𝑈 → (𝑤 = (𝑔 “ {𝑢}) → 𝑤𝑢)))
11995, 118reximdai 3273 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤𝑢))
12090, 119mpd 15 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤𝑢)
121120ralrimiva 3152 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))∃𝑢𝑈 𝑤𝑢)
122 vex 3447 . . . . . . . . . 10 𝑔 ∈ V
123122rnex 7603 . . . . . . . . 9 ran 𝑔 ∈ V
124123mptex 6967 . . . . . . . 8 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V
125 rnexg 7599 . . . . . . . 8 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
126124, 125mp1i 13 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
127 eqid 2801 . . . . . . . 8 ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
128127, 30isref 22118 . . . . . . 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 712 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈)
13115ad2antrr 725 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝐽 ∈ Top)
132 locfinref.2 . . . . . . . 8 (𝜑𝑋 = 𝑈)
133132ad2antrr 725 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = 𝑈)
134133, 83eqtrd 2836 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
135 nfv 1915 . . . . . . . . 9 𝑣 𝑥𝑋
13636, 135nfan 1900 . . . . . . . 8 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋)
137 simplr 768 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → 𝑣𝐽)
138 ffun 6494 . . . . . . . . . . . . . 14 (𝑔:𝑉𝑈 → Fun 𝑔)
139138ad6antlr 736 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔)
140 imafi 8805 . . . . . . . . . . . . 13 ((Fun 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
141139, 140sylancom 591 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
142 simp3 1135 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘))
143 sneq 4538 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑘 → {𝑢} = {𝑘})
144143imaeq2d 5900 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑘 → (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
145144unieqd 4817 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑘 (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
146122cnvex 7616 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔 ∈ V
147 imaexg 7606 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ V → (𝑔 “ {𝑘}) ∈ V)
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 “ {𝑘}) ∈ V
149148uniex 7451 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 “ {𝑘}) ∈ V
150145, 9, 149fvmpt 6749 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
1511503ad2ant2 1131 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
152142, 151eqtrd 2836 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = (𝑔 “ {𝑘}))
153152ineq1d 4141 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → (𝑤𝑣) = ( (𝑔 “ {𝑘}) ∩ 𝑣))
154153neeq1d 3049 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑤𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅))
155123a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V)
156 imaexg 7606 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ V → (𝑔 “ {𝑢}) ∈ V)
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑔 “ {𝑢}) ∈ V
158157uniex 7451 . . . . . . . . . . . . . . . . . . 19 (𝑔 “ {𝑢}) ∈ V
159158, 9fnmpti 6467 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔
160 dffn4 6575 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
161159, 160mpbi 233 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
162161a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
163154, 155, 162rabfodom 30278 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅})
164 sneq 4538 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑢 → {𝑘} = {𝑢})
165164imaeq2d 5900 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑢 → (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
166165unieqd 4817 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
167166ineq1d 4141 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → ( (𝑔 “ {𝑘}) ∩ 𝑣) = ( (𝑔 “ {𝑢}) ∩ 𝑣))
168167neeq1d 3049 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑢 → (( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅))
169168cbvrabv 3442 . . . . . . . . . . . . . . 15 {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}
170163, 169breqtrdi 5074 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅})
171123rabex 5202 . . . . . . . . . . . . . . 15 {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V
172 nfv 1915 . . . . . . . . . . . . . . . . . . . . 21 𝑗(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣)
173 nfrab1 3340 . . . . . . . . . . . . . . . . . . . . . 22 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}
174173nfel1 2974 . . . . . . . . . . . . . . . . . . . . 21 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin
175172, 174nfan 1900 . . . . . . . . . . . . . . . . . . . 20 𝑗((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)
176 nfv 1915 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑢 ∈ ran 𝑔
177175, 176nfan 1900 . . . . . . . . . . . . . . . . . . 19 𝑗(((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔)
178 nfv 1915 . . . . . . . . . . . . . . . . . . 19 𝑗( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅
179177, 178nfan 1900 . . . . . . . . . . . . . . . . . 18 𝑗((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)
180 nfv 1915 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑔𝑘) = 𝑢
181173, 180nfrex 3271 . . . . . . . . . . . . . . . . . 18 𝑗𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢
18239ad5antlr 734 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
183182ad5antr 733 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑔 Fn 𝑉)
184 simplr 768 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ (𝑔 “ {𝑢}))
185 fniniseg 6811 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 Fn 𝑉 → (𝑗 ∈ (𝑔 “ {𝑢}) ↔ (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢)))
186185biimpa 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 Fn 𝑉𝑗 ∈ (𝑔 “ {𝑢})) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
187183, 184, 186syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
188187simpld 498 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗𝑉)
189 simpr 488 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑣) ≠ ∅)
190 rabid 3334 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ↔ (𝑗𝑉 ∧ (𝑗𝑣) ≠ ∅))
191188, 189, 190sylanbrc 586 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})
192187simprd 499 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑔𝑗) = 𝑢)
193 fveqeq2 6658 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝑔𝑘) = 𝑢 ↔ (𝑔𝑗) = 𝑢))
194193rspcev 3574 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∧ (𝑔𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
195191, 192, 194syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
196 uniinn0 30318 . . . . . . . . . . . . . . . . . . . 20 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
197196biimpi 219 . . . . . . . . . . . . . . . . . . 19 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
198197adantl 485 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
199179, 181, 195, 198r19.29af2 3291 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
200199ex 416 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢))
201200ss2rabdv 4006 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
202 ssdomg 8542 . . . . . . . . . . . . . . 15 ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}))
203171, 201, 202mpsyl 68 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
204 domtr 8549 . . . . . . . . . . . . . 14 (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
205170, 203, 204syl2anc 587 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
206182adantr 484 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉)
207 dffn3 6503 . . . . . . . . . . . . . . 15 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
208207biimpi 219 . . . . . . . . . . . . . 14 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
209 ssrab2 4010 . . . . . . . . . . . . . . 15 {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉
210 fimarab 30408 . . . . . . . . . . . . . . 15 ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
211209, 210mpan2 690 . . . . . . . . . . . . . 14 (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
212206, 208, 2113syl 18 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
213205, 212breqtrrd 5061 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}))
214 domfi 8727 . . . . . . . . . . . 12 (((𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
215141, 213, 214syl2anc 587 . . . . . . . . . . 11 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
216215ex 416 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → ({𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
217216imdistanda 575 . . . . . . . . 9 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) → ((𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
218217imp 410 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
219 simplll 774 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → 𝜑)
220 locfinref.x . . . . . . . . . . . . 13 𝑋 = 𝐽
221220, 29islocfin 22126 . . . . . . . . . . . 12 (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
2222, 221sylib 221 . . . . . . . . . . 11 (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
223222simp3d 1141 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
224223r19.21bi 3176 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
225219, 224sylancom 591 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
226136, 137, 218, 225reximd2a 3274 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
227226ralrimiva 3152 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
228220, 127islocfin 22126 . . . . . 6 (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
229131, 134, 227, 228syl3anbrc 1340 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))
230 funeq 6348 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))))
231 dmeq 5740 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
232231sseq1d 3949 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (dom 𝑓𝑈 ↔ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈))
233 rneq 5774 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
234233sseq1d 3949 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓𝐽 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽))
235230, 232, 2343anbi123d 1433 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)))
236233breq1d 5043 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈))
237233eleq1d 2877 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))
238236, 237anbi12d 633 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))))
239235, 238anbi12d 633 . . . . . 6 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) ↔ ((Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))))
240124, 239spcev 3558 . . . . 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 1375 . . . 4 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
242241expl 461 . . 3 (𝜑 → ((𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
243242exlimdv 1934 . 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 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2112  wne 2990  wral 3109  wrex 3110  {crab 3113  Vcvv 3444  cin 3883  wss 3884  c0 4246  {csn 4528   cuni 4803   ciun 4884   class class class wbr 5033  cmpt 5113  ccnv 5522  dom cdm 5523  ran crn 5524  cima 5526  Fun wfun 6322   Fn wfn 6323  wf 6324  ontowfo 6326  cfv 6328  cdom 8494  Fincfn 8496  Topctop 21502  Refcref 22111  LocFinclocfin 22113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-reg 9044  ax-inf2 9092  ax-ac2 9878
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-er 8276  df-en 8497  df-dom 8498  df-fin 8500  df-r1 9181  df-rank 9182  df-card 9356  df-ac 9531  df-top 21503  df-ref 22114  df-locfin 22116
This theorem is referenced by:  locfinref  31198
  Copyright terms: Public domain W3C validator