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 30255
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 30254 . . . . 5 (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
42, 3syl 17 . . . 4 (𝜑 → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
51, 4mpbid 223 . . 3 (𝜑 → ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))))
65simprd 485 . 2 (𝜑 → ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))
7 funmpt 6149 . . . . . 6 Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
87a1i 11 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
9 eqid 2817 . . . . . . 7 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
109dmmptss 5859 . . . . . 6 dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ ran 𝑔
11 frn 6272 . . . . . . 7 (𝑔:𝑉𝑈 → ran 𝑔𝑈)
1211ad2antlr 709 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran 𝑔𝑈)
1310, 12syl5ss 3820 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈)
14 locfintop 21559 . . . . . . . . . 10 (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
152, 14syl 17 . . . . . . . . 9 (𝜑𝐽 ∈ Top)
1615ad3antrrr 712 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top)
17 cnvimass 5709 . . . . . . . . . 10 (𝑔 “ {𝑢}) ⊆ dom 𝑔
18 fdm 6274 . . . . . . . . . . 11 (𝑔:𝑉𝑈 → dom 𝑔 = 𝑉)
1918ad3antlr 713 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉)
2017, 19syl5sseq 3861 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝑉)
21 locfinref.3 . . . . . . . . . 10 (𝜑𝑉𝐽)
2221ad3antrrr 712 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉𝐽)
2320, 22sstrd 3819 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝐽)
24 uniopn 20936 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝑔 “ {𝑢}) ⊆ 𝐽) → (𝑔 “ {𝑢}) ∈ 𝐽)
2516, 23, 24syl2anc 575 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ∈ 𝐽)
2625ralrimiva 3165 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽)
279rnmptss 6624 . . . . . 6 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
2826, 27syl 17 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
29 eqid 2817 . . . . . . . . . 10 𝑉 = 𝑉
30 eqid 2817 . . . . . . . . . 10 𝑈 = 𝑈
3129, 30refbas 21548 . . . . . . . . 9 (𝑉Ref𝑈 𝑈 = 𝑉)
321, 31syl 17 . . . . . . . 8 (𝜑 𝑈 = 𝑉)
3332ad2antrr 708 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = 𝑉)
34 nfv 2005 . . . . . . . . . . . . 13 𝑣(𝜑𝑔:𝑉𝑈)
35 nfra1 3140 . . . . . . . . . . . . 13 𝑣𝑣𝑉 𝑣 ⊆ (𝑔𝑣)
3634, 35nfan 1990 . . . . . . . . . . . 12 𝑣((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
37 nfre1 3203 . . . . . . . . . . . 12 𝑣𝑣𝑉 𝑥𝑣
3836, 37nfan 1990 . . . . . . . . . . 11 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣)
39 ffn 6266 . . . . . . . . . . . . . . 15 (𝑔:𝑉𝑈𝑔 Fn 𝑉)
4039ad4antlr 717 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
41 simplr 776 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑣𝑉)
42 fnfvelrn 6588 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑉𝑣𝑉) → (𝑔𝑣) ∈ ran 𝑔)
4340, 41, 42syl2anc 575 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → (𝑔𝑣) ∈ ran 𝑔)
44 ssid 3831 . . . . . . . . . . . . . . 15 𝑣𝑣
4539ad3antlr 713 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑔 Fn 𝑉)
46 eqid 2817 . . . . . . . . . . . . . . . . 17 (𝑔𝑣) = (𝑔𝑣)
47 fniniseg 6570 . . . . . . . . . . . . . . . . . 18 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {(𝑔𝑣)}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))))
4847biimpar 465 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn 𝑉 ∧ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
4946, 48mpanr2 687 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝑉𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
5045, 49sylancom 578 . . . . . . . . . . . . . . 15 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
51 ssuni 4665 . . . . . . . . . . . . . . 15 ((𝑣𝑣𝑣 ∈ (𝑔 “ {(𝑔𝑣)})) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5244, 50, 51sylancr 577 . . . . . . . . . . . . . 14 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5352sselda 3809 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑥 (𝑔 “ {(𝑔𝑣)}))
54 sneq 4391 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑔𝑣) → {𝑢} = {(𝑔𝑣)})
5554imaeq2d 5690 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5655unieqd 4651 . . . . . . . . . . . . . . 15 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5756eleq2d 2882 . . . . . . . . . . . . . 14 (𝑢 = (𝑔𝑣) → (𝑥 (𝑔 “ {𝑢}) ↔ 𝑥 (𝑔 “ {(𝑔𝑣)})))
5857rspcev 3513 . . . . . . . . . . . . 13 (((𝑔𝑣) ∈ ran 𝑔𝑥 (𝑔 “ {(𝑔𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
5943, 53, 58syl2anc 575 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
6059adantllr 701 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
61 simpr 473 . . . . . . . . . . 11 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑣𝑉 𝑥𝑣)
6238, 60, 61r19.29af 3275 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
63 nfv 2005 . . . . . . . . . . . . . 14 𝑣 𝑢 ∈ ran 𝑔
6436, 63nfan 1990 . . . . . . . . . . . . 13 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔)
65 nfv 2005 . . . . . . . . . . . . 13 𝑣 𝑥 (𝑔 “ {𝑢})
6664, 65nfan 1990 . . . . . . . . . . . 12 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢}))
6720ad3antrrr 712 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → (𝑔 “ {𝑢}) ⊆ 𝑉)
68 simplr 776 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣 ∈ (𝑔 “ {𝑢}))
6967, 68sseldd 3810 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣𝑉)
70 simpr 473 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑥𝑣)
71 simpr 473 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → 𝑥 (𝑔 “ {𝑢}))
72 eluni2 4645 . . . . . . . . . . . . 13 (𝑥 (𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7371, 72sylib 209 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7466, 69, 70, 73reximd2a 3211 . . . . . . . . . . 11 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7574r19.29an 3276 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7662, 75impbida 826 . . . . . . . . 9 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (∃𝑣𝑉 𝑥𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})))
77 eluni2 4645 . . . . . . . . 9 (𝑥 𝑉 ↔ ∃𝑣𝑉 𝑥𝑣)
78 eliun 4727 . . . . . . . . 9 (𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
7976, 77, 783bitr4g 305 . . . . . . . 8 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑥 𝑉𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8079eqrdv 2815 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑉 = 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
81 dfiun3g 5593 . . . . . . . 8 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8226, 81syl 17 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8333, 80, 823eqtrd 2855 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8411ad3antlr 713 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ran 𝑔𝑈)
85 vex 3405 . . . . . . . . . . 11 𝑤 ∈ V
869elrnmpt 5587 . . . . . . . . . . 11 (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8785, 86mp1i 13 . . . . . . . . . 10 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8887biimpa 464 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}))
89 ssrexv 3875 . . . . . . . . 9 (ran 𝑔𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢})))
9084, 88, 89sylc 65 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}))
91 nfv 2005 . . . . . . . . . 10 𝑢((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
92 nfmpt1 4952 . . . . . . . . . . . 12 𝑢(𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9392nfrn 5583 . . . . . . . . . . 11 𝑢ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9493nfcri 2953 . . . . . . . . . 10 𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9591, 94nfan 1990 . . . . . . . . 9 𝑢(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
96 simpr 473 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤 = (𝑔 “ {𝑢}))
97 nfv 2005 . . . . . . . . . . . . . . . 16 𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9836, 97nfan 1990 . . . . . . . . . . . . . . 15 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
99 nfv 2005 . . . . . . . . . . . . . . 15 𝑣 𝑢𝑈
10098, 99nfan 1990 . . . . . . . . . . . . . 14 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈)
101 nfv 2005 . . . . . . . . . . . . . 14 𝑣 𝑤 = (𝑔 “ {𝑢})
102100, 101nfan 1990 . . . . . . . . . . . . 13 𝑣(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢}))
103 simp-5r 798 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
10439ad5antlr 721 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑔 Fn 𝑉)
105 fniniseg 6570 . . . . . . . . . . . . . . . . . . 19 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
106104, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
107106biimpa 464 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢))
108107simpld 484 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑉)
109 rspa 3129 . . . . . . . . . . . . . . . 16 ((∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣) ∧ 𝑣𝑉) → 𝑣 ⊆ (𝑔𝑣))
110103, 108, 109syl2anc 575 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔𝑣))
111107simprd 485 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑔𝑣) = 𝑢)
112110, 111sseqtrd 3849 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑢)
113112ex 399 . . . . . . . . . . . . 13 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) → 𝑣𝑢))
114102, 113ralrimi 3156 . . . . . . . . . . . 12 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
115 unissb 4674 . . . . . . . . . . . 12 ( (𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
116114, 115sylibr 225 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑔 “ {𝑢}) ⊆ 𝑢)
11796, 116eqsstrd 3847 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤𝑢)
118117exp31 408 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (𝑢𝑈 → (𝑤 = (𝑔 “ {𝑢}) → 𝑤𝑢)))
11995, 118reximdai 3210 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤𝑢))
12090, 119mpd 15 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤𝑢)
121120ralrimiva 3165 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))∃𝑢𝑈 𝑤𝑢)
122 vex 3405 . . . . . . . . . 10 𝑔 ∈ V
123122rnex 7340 . . . . . . . . 9 ran 𝑔 ∈ V
124123mptex 6721 . . . . . . . 8 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V
125 rnexg 7338 . . . . . . . 8 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
126124, 125mp1i 13 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
127 eqid 2817 . . . . . . . 8 ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
128127, 30isref 21547 . . . . . . 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 695 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈)
13115ad2antrr 708 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝐽 ∈ Top)
132 locfinref.2 . . . . . . . 8 (𝜑𝑋 = 𝑈)
133132ad2antrr 708 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = 𝑈)
134133, 83eqtrd 2851 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
135 nfv 2005 . . . . . . . . 9 𝑣 𝑥𝑋
13636, 135nfan 1990 . . . . . . . 8 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋)
137 simplr 776 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → 𝑣𝐽)
138 ffun 6269 . . . . . . . . . . . . . 14 (𝑔:𝑉𝑈 → Fun 𝑔)
139138ad6antlr 725 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔)
140 imafi 8508 . . . . . . . . . . . . 13 ((Fun 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
141139, 140sylancom 578 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
142 simp3 1161 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘))
143 sneq 4391 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑘 → {𝑢} = {𝑘})
144143imaeq2d 5690 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑘 → (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
145144unieqd 4651 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑘 (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
146122cnvex 7353 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔 ∈ V
147 imaexg 7343 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ V → (𝑔 “ {𝑘}) ∈ V)
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 “ {𝑘}) ∈ V
149148uniex 7193 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 “ {𝑘}) ∈ V
150145, 9, 149fvmpt 6513 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
1511503ad2ant2 1157 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
152142, 151eqtrd 2851 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = (𝑔 “ {𝑘}))
153152ineq1d 4023 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → (𝑤𝑣) = ( (𝑔 “ {𝑘}) ∩ 𝑣))
154153neeq1d 3048 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑤𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅))
155123a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V)
156 imaexg 7343 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ V → (𝑔 “ {𝑢}) ∈ V)
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑔 “ {𝑢}) ∈ V
158157uniex 7193 . . . . . . . . . . . . . . . . . . 19 (𝑔 “ {𝑢}) ∈ V
159158, 9fnmpti 6243 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔
160 dffn4 6347 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
161159, 160mpbi 221 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
162161a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
163154, 155, 162rabfodom 29692 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅})
164 sneq 4391 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑢 → {𝑘} = {𝑢})
165164imaeq2d 5690 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑢 → (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
166165unieqd 4651 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
167166ineq1d 4023 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → ( (𝑔 “ {𝑘}) ∩ 𝑣) = ( (𝑔 “ {𝑢}) ∩ 𝑣))
168167neeq1d 3048 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑢 → (( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅))
169168cbvrabv 3400 . . . . . . . . . . . . . . 15 {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}
170163, 169syl6breq 4896 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅})
171123rabex 5020 . . . . . . . . . . . . . . 15 {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V
172 nfv 2005 . . . . . . . . . . . . . . . . . . . . 21 𝑗(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣)
173 nfrab1 3322 . . . . . . . . . . . . . . . . . . . . . 22 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}
174173nfel1 2974 . . . . . . . . . . . . . . . . . . . . 21 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin
175172, 174nfan 1990 . . . . . . . . . . . . . . . . . . . 20 𝑗((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)
176 nfv 2005 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑢 ∈ ran 𝑔
177175, 176nfan 1990 . . . . . . . . . . . . . . . . . . 19 𝑗(((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔)
178 nfv 2005 . . . . . . . . . . . . . . . . . . 19 𝑗( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅
179177, 178nfan 1990 . . . . . . . . . . . . . . . . . 18 𝑗((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)
180 nfv 2005 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑔𝑘) = 𝑢
181173, 180nfrex 3205 . . . . . . . . . . . . . . . . . 18 𝑗𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢
18239ad5antlr 721 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
183182ad5antr 719 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑔 Fn 𝑉)
184 simplr 776 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ (𝑔 “ {𝑢}))
185 fniniseg 6570 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 Fn 𝑉 → (𝑗 ∈ (𝑔 “ {𝑢}) ↔ (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢)))
186185biimpa 464 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 Fn 𝑉𝑗 ∈ (𝑔 “ {𝑢})) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
187183, 184, 186syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
188187simpld 484 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗𝑉)
189 simpr 473 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑣) ≠ ∅)
190 rabid 3315 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ↔ (𝑗𝑉 ∧ (𝑗𝑣) ≠ ∅))
191188, 189, 190sylanbrc 574 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})
192187simprd 485 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑔𝑗) = 𝑢)
193 fveqeq2 6427 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝑔𝑘) = 𝑢 ↔ (𝑔𝑗) = 𝑢))
194193rspcev 3513 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∧ (𝑔𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
195191, 192, 194syl2anc 575 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
196 uniinn0 29714 . . . . . . . . . . . . . . . . . . . 20 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
197196biimpi 207 . . . . . . . . . . . . . . . . . . 19 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
198197adantl 469 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
199179, 181, 195, 198r19.29af2 3274 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
200199ex 399 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢))
201200ss2rabdv 3891 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
202 ssdomg 8248 . . . . . . . . . . . . . . 15 ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}))
203171, 201, 202mpsyl 68 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
204 domtr 8255 . . . . . . . . . . . . . 14 (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
205170, 203, 204syl2anc 575 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
206182adantr 468 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉)
207 dffn3 6277 . . . . . . . . . . . . . . 15 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
208207biimpi 207 . . . . . . . . . . . . . 14 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
209 ssrab2 3895 . . . . . . . . . . . . . . 15 {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉
210 fimarab 29795 . . . . . . . . . . . . . . 15 ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
211209, 210mpan2 674 . . . . . . . . . . . . . 14 (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
212206, 208, 2113syl 18 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
213205, 212breqtrrd 4883 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}))
214 domfi 8430 . . . . . . . . . . . 12 (((𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
215141, 213, 214syl2anc 575 . . . . . . . . . . 11 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
216215ex 399 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → ({𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
217216imdistanda 563 . . . . . . . . 9 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) → ((𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
218217imp 395 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
219 simplll 782 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → 𝜑)
220 locfinref.x . . . . . . . . . . . . 13 𝑋 = 𝐽
221220, 29islocfin 21555 . . . . . . . . . . . 12 (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
2222, 221sylib 209 . . . . . . . . . . 11 (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
223222simp3d 1167 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
224223r19.21bi 3131 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
225219, 224sylancom 578 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
226136, 137, 218, 225reximd2a 3211 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
227226ralrimiva 3165 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
228220, 127islocfin 21555 . . . . . 6 (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
229131, 134, 227, 228syl3anbrc 1436 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))
230 funeq 6131 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))))
231 dmeq 5539 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
232231sseq1d 3840 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (dom 𝑓𝑈 ↔ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈))
233 rneq 5566 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
234233sseq1d 3840 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓𝐽 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽))
235230, 232, 2343anbi123d 1553 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)))
236233breq1d 4865 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈))
237233eleq1d 2881 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))
238236, 237anbi12d 618 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))))
239235, 238anbi12d 618 . . . . . 6 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) ↔ ((Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))))
240124, 239spcev 3504 . . . . 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 1490 . . . 4 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
242241expl 447 . . 3 (𝜑 → ((𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
243242exlimdv 2024 . 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 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2157  wne 2989  wral 3107  wrex 3108  {crab 3111  Vcvv 3402  cin 3779  wss 3780  c0 4127  {csn 4381   cuni 4641   ciun 4723   class class class wbr 4855  cmpt 4934  ccnv 5323  dom cdm 5324  ran crn 5325  cima 5327  Fun wfun 6105   Fn wfn 6106  wf 6107  ontowfo 6109  cfv 6111  cdom 8200  Fincfn 8202  Topctop 20932  Refcref 21540  LocFinclocfin 21542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-reg 8746  ax-inf2 8795  ax-ac2 9580
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-om 7306  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-1o 7806  df-er 7989  df-en 8203  df-dom 8204  df-fin 8206  df-r1 8884  df-rank 8885  df-card 9058  df-ac 9232  df-top 20933  df-ref 21543  df-locfin 21545
This theorem is referenced by:  locfinref  30256
  Copyright terms: Public domain W3C validator