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 29881
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 29880 . . . . 5 (𝑉 ∈ (LocFin‘𝐽) → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
42, 3syl 17 . . . 4 (𝜑 → (𝑉Ref𝑈 ↔ ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))))
51, 4mpbid 222 . . 3 (𝜑 → ( 𝑈 𝑉 ∧ ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))))
65simprd 479 . 2 (𝜑 → ∃𝑔(𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)))
7 funmpt 5914 . . . . . 6 Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
87a1i 11 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
9 eqid 2620 . . . . . . 7 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
109dmmptss 5619 . . . . . 6 dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ ran 𝑔
11 frn 6040 . . . . . . 7 (𝑔:𝑉𝑈 → ran 𝑔𝑈)
1211ad2antlr 762 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran 𝑔𝑈)
1310, 12syl5ss 3606 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈)
14 locfintop 21305 . . . . . . . . . 10 (𝑉 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top)
152, 14syl 17 . . . . . . . . 9 (𝜑𝐽 ∈ Top)
1615ad3antrrr 765 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝐽 ∈ Top)
17 cnvimass 5473 . . . . . . . . . 10 (𝑔 “ {𝑢}) ⊆ dom 𝑔
18 fdm 6038 . . . . . . . . . . 11 (𝑔:𝑉𝑈 → dom 𝑔 = 𝑉)
1918ad3antlr 766 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → dom 𝑔 = 𝑉)
2017, 19syl5sseq 3645 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝑉)
21 locfinref.3 . . . . . . . . . 10 (𝜑𝑉𝐽)
2221ad3antrrr 765 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → 𝑉𝐽)
2320, 22sstrd 3605 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ⊆ 𝐽)
24 uniopn 20683 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝑔 “ {𝑢}) ⊆ 𝐽) → (𝑔 “ {𝑢}) ∈ 𝐽)
2516, 23, 24syl2anc 692 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) → (𝑔 “ {𝑢}) ∈ 𝐽)
2625ralrimiva 2963 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽)
279rnmptss 6378 . . . . . 6 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
2826, 27syl 17 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)
29 eqid 2620 . . . . . . . . . 10 𝑉 = 𝑉
30 eqid 2620 . . . . . . . . . 10 𝑈 = 𝑈
3129, 30refbas 21294 . . . . . . . . 9 (𝑉Ref𝑈 𝑈 = 𝑉)
321, 31syl 17 . . . . . . . 8 (𝜑 𝑈 = 𝑉)
3332ad2antrr 761 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = 𝑉)
34 nfv 1841 . . . . . . . . . . . . 13 𝑣(𝜑𝑔:𝑉𝑈)
35 nfra1 2938 . . . . . . . . . . . . 13 𝑣𝑣𝑉 𝑣 ⊆ (𝑔𝑣)
3634, 35nfan 1826 . . . . . . . . . . . 12 𝑣((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
37 nfre1 3002 . . . . . . . . . . . 12 𝑣𝑣𝑉 𝑥𝑣
3836, 37nfan 1826 . . . . . . . . . . 11 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣)
39 ffn 6032 . . . . . . . . . . . . . . 15 (𝑔:𝑉𝑈𝑔 Fn 𝑉)
4039ad4antlr 768 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
41 simplr 791 . . . . . . . . . . . . . 14 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑣𝑉)
42 fnfvelrn 6342 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑉𝑣𝑉) → (𝑔𝑣) ∈ ran 𝑔)
4340, 41, 42syl2anc 692 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → (𝑔𝑣) ∈ ran 𝑔)
44 ssid 3616 . . . . . . . . . . . . . . 15 𝑣𝑣
4539ad3antlr 766 . . . . . . . . . . . . . . . 16 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑔 Fn 𝑉)
46 eqid 2620 . . . . . . . . . . . . . . . . 17 (𝑔𝑣) = (𝑔𝑣)
47 fniniseg 6324 . . . . . . . . . . . . . . . . . 18 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {(𝑔𝑣)}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))))
4847biimpar 502 . . . . . . . . . . . . . . . . 17 ((𝑔 Fn 𝑉 ∧ (𝑣𝑉 ∧ (𝑔𝑣) = (𝑔𝑣))) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
4946, 48mpanr2 719 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝑉𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
5045, 49sylancom 700 . . . . . . . . . . . . . . 15 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 ∈ (𝑔 “ {(𝑔𝑣)}))
51 ssuni 4450 . . . . . . . . . . . . . . 15 ((𝑣𝑣𝑣 ∈ (𝑔 “ {(𝑔𝑣)})) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5244, 50, 51sylancr 694 . . . . . . . . . . . . . 14 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) → 𝑣 (𝑔 “ {(𝑔𝑣)}))
5352sselda 3595 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → 𝑥 (𝑔 “ {(𝑔𝑣)}))
54 sneq 4178 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑔𝑣) → {𝑢} = {(𝑔𝑣)})
5554imaeq2d 5454 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5655unieqd 4437 . . . . . . . . . . . . . . 15 (𝑢 = (𝑔𝑣) → (𝑔 “ {𝑢}) = (𝑔 “ {(𝑔𝑣)}))
5756eleq2d 2685 . . . . . . . . . . . . . 14 (𝑢 = (𝑔𝑣) → (𝑥 (𝑔 “ {𝑢}) ↔ 𝑥 (𝑔 “ {(𝑔𝑣)})))
5857rspcev 3304 . . . . . . . . . . . . 13 (((𝑔𝑣) ∈ ran 𝑔𝑥 (𝑔 “ {(𝑔𝑣)})) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
5943, 53, 58syl2anc 692 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
6059adantllr 754 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) ∧ 𝑣𝑉) ∧ 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
61 simpr 477 . . . . . . . . . . 11 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑣𝑉 𝑥𝑣)
6238, 60, 61r19.29af 3072 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑣𝑉 𝑥𝑣) → ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
63 nfv 1841 . . . . . . . . . . . . . 14 𝑣 𝑢 ∈ ran 𝑔
6436, 63nfan 1826 . . . . . . . . . . . . 13 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔)
65 nfv 1841 . . . . . . . . . . . . 13 𝑣 𝑥 (𝑔 “ {𝑢})
6664, 65nfan 1826 . . . . . . . . . . . 12 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢}))
6720ad3antrrr 765 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → (𝑔 “ {𝑢}) ⊆ 𝑉)
68 simplr 791 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣 ∈ (𝑔 “ {𝑢}))
6967, 68sseldd 3596 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑣𝑉)
70 simpr 477 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) ∧ 𝑥𝑣) → 𝑥𝑣)
71 simpr 477 . . . . . . . . . . . . 13 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → 𝑥 (𝑔 “ {𝑢}))
72 eluni2 4431 . . . . . . . . . . . . 13 (𝑥 (𝑔 “ {𝑢}) ↔ ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7371, 72sylib 208 . . . . . . . . . . . 12 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣 ∈ (𝑔 “ {𝑢})𝑥𝑣)
7466, 69, 70, 73reximd2a 3010 . . . . . . . . . . 11 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑢 ∈ ran 𝑔) ∧ 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7574r19.29an 3073 . . . . . . . . . 10 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})) → ∃𝑣𝑉 𝑥𝑣)
7662, 75impbida 876 . . . . . . . . 9 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (∃𝑣𝑉 𝑥𝑣 ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢})))
77 eluni2 4431 . . . . . . . . 9 (𝑥 𝑉 ↔ ∃𝑣𝑉 𝑥𝑣)
78 eliun 4515 . . . . . . . . 9 (𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ↔ ∃𝑢 ∈ ran 𝑔 𝑥 (𝑔 “ {𝑢}))
7976, 77, 783bitr4g 303 . . . . . . . 8 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑥 𝑉𝑥 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8079eqrdv 2618 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑉 = 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
81 dfiun3g 5367 . . . . . . . 8 (∀𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) ∈ 𝐽 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8226, 81syl 17 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8333, 80, 823eqtrd 2658 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑈 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
8411ad3antlr 766 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ran 𝑔𝑈)
85 vex 3198 . . . . . . . . . . 11 𝑤 ∈ V
869elrnmpt 5361 . . . . . . . . . . 11 (𝑤 ∈ V → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8785, 86mp1i 13 . . . . . . . . . 10 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → (𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ↔ ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢})))
8887biimpa 501 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}))
89 ssrexv 3659 . . . . . . . . 9 (ran 𝑔𝑈 → (∃𝑢 ∈ ran 𝑔 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢})))
9084, 88, 89sylc 65 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}))
91 nfv 1841 . . . . . . . . . 10 𝑢((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
92 nfmpt1 4738 . . . . . . . . . . . 12 𝑢(𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9392nfrn 5357 . . . . . . . . . . 11 𝑢ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9493nfcri 2756 . . . . . . . . . 10 𝑢 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9591, 94nfan 1826 . . . . . . . . 9 𝑢(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
96 simpr 477 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤 = (𝑔 “ {𝑢}))
97 nfv 1841 . . . . . . . . . . . . . . . 16 𝑣 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
9836, 97nfan 1826 . . . . . . . . . . . . . . 15 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
99 nfv 1841 . . . . . . . . . . . . . . 15 𝑣 𝑢𝑈
10098, 99nfan 1826 . . . . . . . . . . . . . 14 𝑣((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈)
101 nfv 1841 . . . . . . . . . . . . . 14 𝑣 𝑤 = (𝑔 “ {𝑢})
102100, 101nfan 1826 . . . . . . . . . . . . 13 𝑣(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢}))
103 simp-5r 808 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣))
10439ad5antlr 770 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑔 Fn 𝑉)
105 fniniseg 6324 . . . . . . . . . . . . . . . . . . 19 (𝑔 Fn 𝑉 → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
106104, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) ↔ (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢)))
107106biimpa 501 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑣𝑉 ∧ (𝑔𝑣) = 𝑢))
108107simpld 475 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑉)
109 rspa 2927 . . . . . . . . . . . . . . . 16 ((∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣) ∧ 𝑣𝑉) → 𝑣 ⊆ (𝑔𝑣))
110103, 108, 109syl2anc 692 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣 ⊆ (𝑔𝑣))
111107simprd 479 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → (𝑔𝑣) = 𝑢)
112110, 111sseqtrd 3633 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) ∧ 𝑣 ∈ (𝑔 “ {𝑢})) → 𝑣𝑢)
113112ex 450 . . . . . . . . . . . . 13 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑣 ∈ (𝑔 “ {𝑢}) → 𝑣𝑢))
114102, 113ralrimi 2954 . . . . . . . . . . . 12 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
115 unissb 4460 . . . . . . . . . . . 12 ( (𝑔 “ {𝑢}) ⊆ 𝑢 ↔ ∀𝑣 ∈ (𝑔 “ {𝑢})𝑣𝑢)
116114, 115sylibr 224 . . . . . . . . . . 11 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → (𝑔 “ {𝑢}) ⊆ 𝑢)
11796, 116eqsstrd 3631 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) ∧ 𝑢𝑈) ∧ 𝑤 = (𝑔 “ {𝑢})) → 𝑤𝑢)
118117exp31 629 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (𝑢𝑈 → (𝑤 = (𝑔 “ {𝑢}) → 𝑤𝑢)))
11995, 118reximdai 3009 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → (∃𝑢𝑈 𝑤 = (𝑔 “ {𝑢}) → ∃𝑢𝑈 𝑤𝑢))
12090, 119mpd 15 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))) → ∃𝑢𝑈 𝑤𝑢)
121120ralrimiva 2963 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))∃𝑢𝑈 𝑤𝑢)
122 vex 3198 . . . . . . . . . 10 𝑔 ∈ V
123122rnex 7085 . . . . . . . . 9 ran 𝑔 ∈ V
124123mptex 6471 . . . . . . . 8 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V
125 rnexg 7083 . . . . . . . 8 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
126124, 125mp1i 13 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ V)
127 eqid 2620 . . . . . . . 8 ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
128127, 30isref 21293 . . . . . . 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 956 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈)
13115ad2antrr 761 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝐽 ∈ Top)
132 locfinref.2 . . . . . . . 8 (𝜑𝑋 = 𝑈)
133132ad2antrr 761 . . . . . . 7 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = 𝑈)
134133, 83eqtrd 2654 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
135 nfv 1841 . . . . . . . . 9 𝑣 𝑥𝑋
13636, 135nfan 1826 . . . . . . . 8 𝑣(((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋)
137 simplr 791 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → 𝑣𝐽)
138 ffun 6035 . . . . . . . . . . . . . 14 (𝑔:𝑉𝑈 → Fun 𝑔)
139138ad6antlr 772 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → Fun 𝑔)
140 imafi 8244 . . . . . . . . . . . . 13 ((Fun 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
141139, 140sylancom 700 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin)
142 simp3 1061 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘))
143 sneq 4178 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑘 → {𝑢} = {𝑘})
144143imaeq2d 5454 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑘 → (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
145144unieqd 4437 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝑘 (𝑔 “ {𝑢}) = (𝑔 “ {𝑘}))
146122cnvex 7098 . . . . . . . . . . . . . . . . . . . . . . 23 𝑔 ∈ V
147 imaexg 7088 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 ∈ V → (𝑔 “ {𝑘}) ∈ V)
148146, 147ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 “ {𝑘}) ∈ V
149148uniex 6938 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 “ {𝑘}) ∈ V
150145, 9, 149fvmpt 6269 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ran 𝑔 → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
1511503ad2ant2 1081 . . . . . . . . . . . . . . . . . . 19 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘) = (𝑔 “ {𝑘}))
152142, 151eqtrd 2654 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → 𝑤 = (𝑔 “ {𝑘}))
153152ineq1d 3805 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → (𝑤𝑣) = ( (𝑔 “ {𝑘}) ∩ 𝑣))
154153neeq1d 2850 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑘 ∈ ran 𝑔𝑤 = ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))‘𝑘)) → ((𝑤𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅))
155123a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → ran 𝑔 ∈ V)
156 imaexg 7088 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ V → (𝑔 “ {𝑢}) ∈ V)
157146, 156ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑔 “ {𝑢}) ∈ V
158157uniex 6938 . . . . . . . . . . . . . . . . . . 19 (𝑔 “ {𝑢}) ∈ V
159158, 9fnmpti 6009 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔
160 dffn4 6108 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) Fn ran 𝑔 ↔ (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
161159, 160mpbi 220 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))
162161a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})):ran 𝑔onto→ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
163154, 155, 162rabfodom 29316 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅})
164 sneq 4178 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑢 → {𝑘} = {𝑢})
165164imaeq2d 5454 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑢 → (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
166165unieqd 4437 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑢 (𝑔 “ {𝑘}) = (𝑔 “ {𝑢}))
167166ineq1d 3805 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑢 → ( (𝑔 “ {𝑘}) ∩ 𝑣) = ( (𝑔 “ {𝑢}) ∩ 𝑣))
168167neeq1d 2850 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑢 → (( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅ ↔ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅))
169168cbvrabv 3194 . . . . . . . . . . . . . . 15 {𝑘 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑘}) ∩ 𝑣) ≠ ∅} = {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅}
170163, 169syl6breq 4685 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅})
171123rabex 4804 . . . . . . . . . . . . . . 15 {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V
172 nfv 1841 . . . . . . . . . . . . . . . . . . . . 21 𝑗(((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣)
173 nfrab1 3117 . . . . . . . . . . . . . . . . . . . . . 22 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}
174173nfel1 2776 . . . . . . . . . . . . . . . . . . . . 21 𝑗{𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin
175172, 174nfan 1826 . . . . . . . . . . . . . . . . . . . 20 𝑗((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)
176 nfv 1841 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑢 ∈ ran 𝑔
177175, 176nfan 1826 . . . . . . . . . . . . . . . . . . 19 𝑗(((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔)
178 nfv 1841 . . . . . . . . . . . . . . . . . . 19 𝑗( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅
179177, 178nfan 1826 . . . . . . . . . . . . . . . . . 18 𝑗((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅)
180 nfv 1841 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑔𝑘) = 𝑢
181173, 180nfrex 3004 . . . . . . . . . . . . . . . . . 18 𝑗𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢
18239ad5antlr 770 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → 𝑔 Fn 𝑉)
183182ad5antr 769 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑔 Fn 𝑉)
184 simplr 791 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ (𝑔 “ {𝑢}))
185 fniniseg 6324 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 Fn 𝑉 → (𝑗 ∈ (𝑔 “ {𝑢}) ↔ (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢)))
186185biimpa 501 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 Fn 𝑉𝑗 ∈ (𝑔 “ {𝑢})) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
187183, 184, 186syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑉 ∧ (𝑔𝑗) = 𝑢))
188187simpld 475 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗𝑉)
189 simpr 477 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑗𝑣) ≠ ∅)
190 rabid 3111 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ↔ (𝑗𝑉 ∧ (𝑗𝑣) ≠ ∅))
191188, 189, 190sylanbrc 697 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → 𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})
192187simprd 479 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → (𝑔𝑗) = 𝑢)
193 fveq2 6178 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑗 → (𝑔𝑘) = (𝑔𝑗))
194193eqeq1d 2622 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝑔𝑘) = 𝑢 ↔ (𝑔𝑗) = 𝑢))
195194rspcev 3304 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∧ (𝑔𝑗) = 𝑢) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
196191, 192, 195syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) ∧ 𝑗 ∈ (𝑔 “ {𝑢})) ∧ (𝑗𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
197 uniinn0 29338 . . . . . . . . . . . . . . . . . . . 20 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ ↔ ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
198197biimpi 206 . . . . . . . . . . . . . . . . . . 19 (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
199198adantl 482 . . . . . . . . . . . . . . . . . 18 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑗 ∈ (𝑔 “ {𝑢})(𝑗𝑣) ≠ ∅)
200179, 181, 196, 199r19.29af2 3071 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) ∧ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅) → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢)
201200ex 450 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) ∧ 𝑢 ∈ ran 𝑔) → (( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅ → ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢))
202201ss2rabdv 3675 . . . . . . . . . . . . . . 15 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
203 ssdomg 7986 . . . . . . . . . . . . . . 15 ({𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} ∈ V → ({𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ⊆ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢} → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}))
204171, 202, 203mpsyl 68 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
205 domtr 7994 . . . . . . . . . . . . . 14 (({𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ∧ {𝑢 ∈ ran 𝑔 ∣ ( (𝑔 “ {𝑢}) ∩ 𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢}) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
206170, 204, 205syl2anc 692 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
207182adantr 481 . . . . . . . . . . . . . 14 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → 𝑔 Fn 𝑉)
208 dffn3 6041 . . . . . . . . . . . . . . 15 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
209208biimpi 206 . . . . . . . . . . . . . 14 (𝑔 Fn 𝑉𝑔:𝑉⟶ran 𝑔)
210 ssrab2 3679 . . . . . . . . . . . . . . 15 {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉
211 fimarab 29418 . . . . . . . . . . . . . . 15 ((𝑔:𝑉⟶ran 𝑔 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ⊆ 𝑉) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
212210, 211mpan2 706 . . . . . . . . . . . . . 14 (𝑔:𝑉⟶ran 𝑔 → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
213207, 209, 2123syl 18 . . . . . . . . . . . . 13 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) = {𝑢 ∈ ran 𝑔 ∣ ∃𝑘 ∈ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} (𝑔𝑘) = 𝑢})
214206, 213breqtrrd 4672 . . . . . . . . . . . 12 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}))
215 domfi 8166 . . . . . . . . . . . 12 (((𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅}) ∈ Fin ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ≼ (𝑔 “ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅})) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
216141, 214, 215syl2anc 692 . . . . . . . . . . 11 (((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)
217216ex 450 . . . . . . . . . 10 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ 𝑥𝑣) → ({𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin → {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
218217imdistanda 728 . . . . . . . . 9 (((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) → ((𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
219218imp 445 . . . . . . . 8 ((((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) ∧ 𝑣𝐽) ∧ (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)) → (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
220 simplll 797 . . . . . . . . 9 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → 𝜑)
221 locfinref.x . . . . . . . . . . . . 13 𝑋 = 𝐽
222221, 29islocfin 21301 . . . . . . . . . . . 12 (𝑉 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
2232, 222sylib 208 . . . . . . . . . . 11 (𝜑 → (𝐽 ∈ Top ∧ 𝑋 = 𝑉 ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin)))
224223simp3d 1073 . . . . . . . . . 10 (𝜑 → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
225224r19.21bi 2929 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
226220, 225sylancom 700 . . . . . . . 8 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑗𝑉 ∣ (𝑗𝑣) ≠ ∅} ∈ Fin))
227136, 137, 219, 226reximd2a 3010 . . . . . . 7 ((((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) ∧ 𝑥𝑋) → ∃𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
228227ralrimiva 2963 . . . . . 6 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin))
229221, 127islocfin 21301 . . . . . 6 (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ ∀𝑥𝑋𝑣𝐽 (𝑥𝑣 ∧ {𝑤 ∈ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∣ (𝑤𝑣) ≠ ∅} ∈ Fin)))
230131, 134, 228, 229syl3anbrc 1244 . . . . 5 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))
231 funeq 5896 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (Fun 𝑓 ↔ Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))))
232 dmeq 5313 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → dom 𝑓 = dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
233232sseq1d 3624 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (dom 𝑓𝑈 ↔ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈))
234 rneq 5340 . . . . . . . . 9 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ran 𝑓 = ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})))
235234sseq1d 3624 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓𝐽 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽))
236231, 233, 2353anbi123d 1397 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ↔ (Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽)))
237234breq1d 4654 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓Ref𝑈 ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈))
238234eleq1d 2684 . . . . . . . 8 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (ran 𝑓 ∈ (LocFin‘𝐽) ↔ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))
239237, 238anbi12d 746 . . . . . . 7 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → ((ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)) ↔ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽))))
240236, 239anbi12d 746 . . . . . 6 (𝑓 = (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) → (((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) ↔ ((Fun (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∧ dom (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ⊆ 𝐽) ∧ (ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢}))Ref𝑈 ∧ ran (𝑢 ∈ ran 𝑔 (𝑔 “ {𝑢})) ∈ (LocFin‘𝐽)))))
241124, 240spcev 3295 . . . . 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 1332 . . . 4 (((𝜑𝑔:𝑉𝑈) ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))))
243242expl 647 . . 3 (𝜑 → ((𝑔:𝑉𝑈 ∧ ∀𝑣𝑉 𝑣 ⊆ (𝑔𝑣)) → ∃𝑓((Fun 𝑓 ∧ dom 𝑓𝑈 ∧ ran 𝑓𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))))
244243exlimdv 1859 . 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 196  wa 384  w3a 1036   = wceq 1481  wex 1702  wcel 1988  wne 2791  wral 2909  wrex 2910  {crab 2913  Vcvv 3195  cin 3566  wss 3567  c0 3907  {csn 4168   cuni 4427   ciun 4511   class class class wbr 4644  cmpt 4720  ccnv 5103  dom cdm 5104  ran crn 5105  cima 5107  Fun wfun 5870   Fn wfn 5871  wf 5872  ontowfo 5874  cfv 5876  cdom 7938  Fincfn 7940  Topctop 20679  Refcref 21286  LocFinclocfin 21288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-reg 8482  ax-inf2 8523  ax-ac2 9270
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-om 7051  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-er 7727  df-en 7941  df-dom 7942  df-fin 7944  df-r1 8612  df-rank 8613  df-card 8750  df-ac 8924  df-top 20680  df-ref 21289  df-locfin 21291
This theorem is referenced by:  locfinref  29882
  Copyright terms: Public domain W3C validator