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 29038
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 29037 . . . . 5 (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
42, 3syl 17 . . . 4 (𝜑 → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
51, 4mpbid 220 . . 3 (𝜑 → ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))))
65simprd 477 . 2 (𝜑 → ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))
7 funmpt 5823 . . . . . 6 Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
87a1i 11 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
9 eqid 2606 . . . . . . 7 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
109dmmptss 5531 . . . . . 6 dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ ran 𝑔
11 frn 5949 . . . . . . 7 (𝑔:𝑉𝑈 → ran 𝑔𝑈)
1211ad2antlr 758 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran 𝑔𝑈)
1310, 12syl5ss 3575 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈)
14 locfintop 21073 . . . . . . . . . 10 (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
152, 14syl 17 . . . . . . . . 9 (𝜑𝐽 ∈ Top)
1615ad3antrrr 761 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top)
17 cnvimass 5388 . . . . . . . . . 10 (𝑔 “ {𝑢}) ⊆ dom 𝑔
18 fdm 5947 . . . . . . . . . . 11 (𝑔:𝑉𝑈 → dom 𝑔 = 𝑉)
1918ad3antlr 762 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉)
2017, 19syl5sseq 3612 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝑉)
21 locfinref.3 . . . . . . . . . 10 (𝜑𝑉𝐽)
2221ad3antrrr 761 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉𝐽)
2320, 22sstrd 3574 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝐽)
24 uniopn 20466 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝑔 “ {𝑢}) ⊆ 𝐽) → (𝑔 “ {𝑢}) ∈ 𝐽)
2516, 23, 24syl2anc 690 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ∈ 𝐽)
2625ralrimiva 2945 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽)
279rnmptss 6281 . . . . . 6 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
2826, 27syl 17 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
29 eqid 2606 . . . . . . . . . 10 𝑉 = 𝑉
30 eqid 2606 . . . . . . . . . 10 𝑈 = 𝑈
3129, 30refbas 21062 . . . . . . . . 9 (𝑉Ref𝑈 𝑈 = 𝑉)
321, 31syl 17 . . . . . . . 8 (𝜑 𝑈 = 𝑉)
3332ad2antrr 757 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = 𝑉)
34 nfv 1829 . . . . . . . . . . . . 13 𝑣(𝜑𝑔:𝑉𝑈)
35 nfra1 2921 . . . . . . . . . . . . 13 𝑣𝑣𝑉 𝑣 ⊆ (𝑔𝑣)
3634, 35nfan 1815 . . . . . . . . . . . 12 𝑣((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
37 nfre1 2984 . . . . . . . . . . . 12 𝑣𝑣𝑉 𝑥𝑣
3836, 37nfan 1815 . . . . . . . . . . 11 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣)
39 ffn 5941 . . . . . . . . . . . . . . 15 (𝑔:𝑉𝑈𝑔 Fn 𝑉)
4039ad4antlr 764 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
41 simplr 787 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑣𝑉)
42 fnfvelrn 6246 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑉𝑣𝑉) → (𝑔𝑣) ∈ ran 𝑔)
4340, 41, 42syl2anc 690 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → (𝑔𝑣) ∈ ran 𝑔)
44 ssid 3583 . . . . . . . . . . . . . . 15 𝑣𝑣
4539ad3antlr 762 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑔 Fn 𝑉)
46 eqid 2606 . . . . . . . . . . . . . . . . 17 (𝑔𝑣) = (𝑔𝑣)
47 fniniseg 6228 . . . . . . . . . . . . . . . . . 18 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {(𝑔𝑣)}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))))
4847biimpar 500 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn 𝑉 ∧ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
4946, 48mpanr2 715 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝑉𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
5045, 49sylancom 697 . . . . . . . . . . . . . . 15 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
51 ssuni 4386 . . . . . . . . . . . . . . 15 ((𝑣𝑣𝑣 ∈ (𝑔 “ {(𝑔𝑣)})) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5244, 50, 51sylancr 693 . . . . . . . . . . . . . 14 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5352sselda 3564 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑥 (𝑔 “ {(𝑔𝑣)}))
54 sneq 4131 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑔𝑣) → {𝑢} = {(𝑔𝑣)})
5554imaeq2d 5369 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5655unieqd 4373 . . . . . . . . . . . . . . 15 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5756eleq2d 2669 . . . . . . . . . . . . . 14 (𝑢 = (𝑔𝑣) → (𝑥 (𝑔 “ {𝑢}) ↔ 𝑥 (𝑔 “ {(𝑔𝑣)})))
5857rspcev 3278 . . . . . . . . . . . . 13 (((𝑔𝑣) ∈ ran 𝑔𝑥 (𝑔 “ {(𝑔𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
5943, 53, 58syl2anc 690 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
6059adantllr 750 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
61 simpr 475 . . . . . . . . . . 11 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑣𝑉 𝑥𝑣)
6238, 60, 61r19.29af 3054 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
63 nfv 1829 . . . . . . . . . . . . . 14 𝑣 𝑢 ∈ ran 𝑔
6436, 63nfan 1815 . . . . . . . . . . . . 13 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔)
65 nfv 1829 . . . . . . . . . . . . 13 𝑣 𝑥 (𝑔 “ {𝑢})
6664, 65nfan 1815 . . . . . . . . . . . 12 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢}))
6720ad3antrrr 761 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → (𝑔 “ {𝑢}) ⊆ 𝑉)
68 simplr 787 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣 ∈ (𝑔 “ {𝑢}))
6967, 68sseldd 3565 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣𝑉)
70 simpr 475 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑥𝑣)
71 simpr 475 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → 𝑥 (𝑔 “ {𝑢}))
72 eluni2 4367 . . . . . . . . . . . . 13 (𝑥 (𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7371, 72sylib 206 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7466, 69, 70, 73reximd2a 2992 . . . . . . . . . . 11 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7574r19.29an 3055 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7662, 75impbida 872 . . . . . . . . 9 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (∃𝑣𝑉 𝑥𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})))
77 eluni2 4367 . . . . . . . . 9 (𝑥 𝑉 ↔ ∃𝑣𝑉 𝑥𝑣)
78 eliun 4451 . . . . . . . . 9 (𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
7976, 77, 783bitr4g 301 . . . . . . . 8 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑥 𝑉𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8079eqrdv 2604 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑉 = 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
81 dfiun3g 5283 . . . . . . . 8 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8226, 81syl 17 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8333, 80, 823eqtrd 2644 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8411ad3antlr 762 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ran 𝑔𝑈)
85 vex 3172 . . . . . . . . . . 11 𝑤 ∈ V
869elrnmpt 5277 . . . . . . . . . . 11 (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8785, 86mp1i 13 . . . . . . . . . 10 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8887biimpa 499 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}))
89 ssrexv 3626 . . . . . . . . 9 (ran 𝑔𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢})))
9084, 88, 89sylc 62 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}))
91 nfv 1829 . . . . . . . . . 10 𝑢((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
92 nfmpt1 4666 . . . . . . . . . . . 12 𝑢(𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9392nfrn 5273 . . . . . . . . . . 11 𝑢ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9493nfcri 2741 . . . . . . . . . 10 𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9591, 94nfan 1815 . . . . . . . . 9 𝑢(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
96 simpr 475 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤 = (𝑔 “ {𝑢}))
97 nfv 1829 . . . . . . . . . . . . . . . 16 𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9836, 97nfan 1815 . . . . . . . . . . . . . . 15 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
99 nfv 1829 . . . . . . . . . . . . . . 15 𝑣 𝑢𝑈
10098, 99nfan 1815 . . . . . . . . . . . . . 14 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈)
101 nfv 1829 . . . . . . . . . . . . . 14 𝑣 𝑤 = (𝑔 “ {𝑢})
102100, 101nfan 1815 . . . . . . . . . . . . 13 𝑣(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢}))
103 simp-5r 804 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
10439ad5antlr 766 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑔 Fn 𝑉)
105 fniniseg 6228 . . . . . . . . . . . . . . . . . . 19 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
106104, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
107106biimpa 499 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢))
108107simpld 473 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑉)
109 rspa 2910 . . . . . . . . . . . . . . . 16 ((∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣) ∧ 𝑣𝑉) → 𝑣 ⊆ (𝑔𝑣))
110103, 108, 109syl2anc 690 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔𝑣))
111107simprd 477 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑔𝑣) = 𝑢)
112110, 111sseqtrd 3600 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑢)
113112ex 448 . . . . . . . . . . . . 13 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) → 𝑣𝑢))
114102, 113ralrimi 2936 . . . . . . . . . . . 12 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
115 unissb 4396 . . . . . . . . . . . 12 ( (𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
116114, 115sylibr 222 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑔 “ {𝑢}) ⊆ 𝑢)
11796, 116eqsstrd 3598 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤𝑢)
118117exp31 627 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (𝑢𝑈 → (𝑤 = (𝑔 “ {𝑢}) → 𝑤𝑢)))
11995, 118reximdai 2991 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤𝑢))
12090, 119mpd 15 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤𝑢)
121120ralrimiva 2945 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))∃𝑢𝑈 𝑤𝑢)
122 vex 3172 . . . . . . . . . 10 𝑔 ∈ V
123122rnex 6966 . . . . . . . . 9 ran 𝑔 ∈ V
124123mptex 6365 . . . . . . . 8 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V
125 rnexg 6964 . . . . . . . 8 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
126124, 125mp1i 13 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
127 eqid 2606 . . . . . . . 8 ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
128127, 30isref 21061 . . . . . . 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 958 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈)
13115ad2antrr 757 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝐽 ∈ Top)
132 locfinref.2 . . . . . . . 8 (𝜑𝑋 = 𝑈)
133132ad2antrr 757 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = 𝑈)
134133, 83eqtrd 2640 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
135 nfv 1829 . . . . . . . . 9 𝑣 𝑥𝑋
13636, 135nfan 1815 . . . . . . . 8 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋)
137 simplr 787 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → 𝑣𝐽)
138 ffun 5944 . . . . . . . . . . . . . 14 (𝑔:𝑉𝑈 → Fun 𝑔)
139138ad6antlr 768 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔)
140 imafi 8116 . . . . . . . . . . . . 13 ((Fun 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
141139, 140sylancom 697 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
142 simp3 1055 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘))
143 sneq 4131 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑘 → {𝑢} = {𝑘})
144143imaeq2d 5369 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑘 → (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
145144unieqd 4373 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑘 (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
146122cnvex 6980 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔 ∈ V
147 imaexg 6969 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ V → (𝑔 “ {𝑘}) ∈ V)
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 “ {𝑘}) ∈ V
149148uniex 6825 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 “ {𝑘}) ∈ V
150145, 9, 149fvmpt 6173 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
1511503ad2ant2 1075 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
152142, 151eqtrd 2640 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = (𝑔 “ {𝑘}))
153152ineq1d 3771 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → (𝑤𝑣) = ( (𝑔 “ {𝑘}) ∩ 𝑣))
154153neeq1d 2837 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑤𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅))
155123a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V)
156 imaexg 6969 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ V → (𝑔 “ {𝑢}) ∈ V)
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑔 “ {𝑢}) ∈ V
158157uniex 6825 . . . . . . . . . . . . . . . . . . 19 (𝑔 “ {𝑢}) ∈ V
159158, 9fnmpti 5918 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔
160 dffn4 6016 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
161159, 160mpbi 218 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
162161a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
163154, 155, 162rabfodom 28531 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅})
164 sneq 4131 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑢 → {𝑘} = {𝑢})
165164imaeq2d 5369 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑢 → (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
166165unieqd 4373 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
167166ineq1d 3771 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → ( (𝑔 “ {𝑘}) ∩ 𝑣) = ( (𝑔 “ {𝑢}) ∩ 𝑣))
168167neeq1d 2837 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑢 → (( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅))
169168cbvrabv 3168 . . . . . . . . . . . . . . 15 {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}
170163, 169syl6breq 4615 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅})
171123rabex 4732 . . . . . . . . . . . . . . 15 {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V
172 nfv 1829 . . . . . . . . . . . . . . . . . . . . 21 𝑗(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣)
173 nfrab1 3095 . . . . . . . . . . . . . . . . . . . . . 22 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}
174173nfel1 2761 . . . . . . . . . . . . . . . . . . . . 21 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin
175172, 174nfan 1815 . . . . . . . . . . . . . . . . . . . 20 𝑗((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)
176 nfv 1829 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑢 ∈ ran 𝑔
177175, 176nfan 1815 . . . . . . . . . . . . . . . . . . 19 𝑗(((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔)
178 nfv 1829 . . . . . . . . . . . . . . . . . . 19 𝑗( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅
179177, 178nfan 1815 . . . . . . . . . . . . . . . . . 18 𝑗((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)
180 nfv 1829 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑔𝑘) = 𝑢
181173, 180nfrex 2986 . . . . . . . . . . . . . . . . . 18 𝑗𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢
18239ad5antlr 766 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
183182ad5antr 765 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑔 Fn 𝑉)
184 simplr 787 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ (𝑔 “ {𝑢}))
185 fniniseg 6228 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 Fn 𝑉 → (𝑗 ∈ (𝑔 “ {𝑢}) ↔ (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢)))
186185biimpa 499 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 Fn 𝑉𝑗 ∈ (𝑔 “ {𝑢})) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
187183, 184, 186syl2anc 690 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
188187simpld 473 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗𝑉)
189 simpr 475 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑣) ≠ ∅)
190 rabid 3091 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ↔ (𝑗𝑉 ∧ (𝑗𝑣) ≠ ∅))
191188, 189, 190sylanbrc 694 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})
192187simprd 477 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑔𝑗) = 𝑢)
193 fveq2 6085 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑗 → (𝑔𝑘) = (𝑔𝑗))
194193eqeq1d 2608 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝑔𝑘) = 𝑢 ↔ (𝑔𝑗) = 𝑢))
195194rspcev 3278 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∧ (𝑔𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
196191, 192, 195syl2anc 690 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
197 uniinn0 28552 . . . . . . . . . . . . . . . . . . . 20 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
198197biimpi 204 . . . . . . . . . . . . . . . . . . 19 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
199198adantl 480 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
200179, 181, 196, 199r19.29af2 3053 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
201200ex 448 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢))
202201ss2rabdv 3642 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
203 ssdomg 7861 . . . . . . . . . . . . . . 15 ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}))
204171, 202, 203mpsyl 65 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
205 domtr 7869 . . . . . . . . . . . . . 14 (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
206170, 204, 205syl2anc 690 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
207182adantr 479 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉)
208 dffn3 5950 . . . . . . . . . . . . . . 15 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
209208biimpi 204 . . . . . . . . . . . . . 14 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
210 ssrab2 3646 . . . . . . . . . . . . . . 15 {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉
211 fimarab 28628 . . . . . . . . . . . . . . 15 ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
212210, 211mpan2 702 . . . . . . . . . . . . . 14 (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
213207, 209, 2123syl 18 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
214206, 213breqtrrd 4602 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}))
215 domfi 8040 . . . . . . . . . . . 12 (((𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
216141, 214, 215syl2anc 690 . . . . . . . . . . 11 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
217216ex 448 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → ({𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
218217imdistanda 724 . . . . . . . . 9 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) → ((𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
219218imp 443 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
220 simplll 793 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → 𝜑)
221 locfinref.x . . . . . . . . . . . . 13 𝑋 = 𝐽
222221, 29islocfin 21069 . . . . . . . . . . . 12 (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
2232, 222sylib 206 . . . . . . . . . . 11 (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
224223simp3d 1067 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
225224r19.21bi 2912 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
226220, 225sylancom 697 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
227136, 137, 219, 226reximd2a 2992 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
228227ralrimiva 2945 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
229221, 127islocfin 21069 . . . . . 6 (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
230131, 134, 228, 229syl3anbrc 1238 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))
231 funeq 5806 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))))
232 dmeq 5230 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
233232sseq1d 3591 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (dom 𝑓𝑈 ↔ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈))
234 rneq 5256 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
235234sseq1d 3591 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓𝐽 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽))
236231, 233, 2353anbi123d 1390 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)))
237234breq1d 4584 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈))
238234eleq1d 2668 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))
239237, 238anbi12d 742 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))))
240236, 239anbi12d 742 . . . . . 6 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) ↔ ((Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))))
241124, 240spcev 3269 . . . . 5 (((Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
2428, 13, 28, 130, 230, 241syl32anc 1325 . . . 4 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
243242expl 645 . . 3 (𝜑 → ((𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
244243exlimdv 1847 . 2 (𝜑 → (∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
2456, 244mpd 15 1 (𝜑 → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1976  wne 2776  wral 2892  wrex 2893  {crab 2896  Vcvv 3169  cin 3535  wss 3536  c0 3870  {csn 4121   cuni 4363   ciun 4446   class class class wbr 4574  cmpt 4634  ccnv 5024  dom cdm 5025  ran crn 5026  cima 5028  Fun wfun 5781   Fn wfn 5782  wf 5783  ontowfo 5785  cfv 5787  cdom 7813  Fincfn 7815  Topctop 20456  Refcref 21054  LocFinclocfin 21056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-reg 8354  ax-inf2 8395  ax-ac2 9142
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-iin 4449  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-om 6932  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-er 7603  df-en 7816  df-dom 7817  df-fin 7819  df-r1 8484  df-rank 8485  df-card 8622  df-ac 8796  df-top 20460  df-ref 21057  df-locfin 21059
This theorem is referenced by:  locfinref  29039
  Copyright terms: Public domain W3C validator