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

Theorem pibt2 35888
Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 35885 and pibp21 35886 for the definitions of the relevant properties. This proof uses the axiom of choice. (Contributed by ML, 30-Mar-2021.)
Hypotheses
Ref Expression
pibt2.x 𝑋 = 𝐽
pibt2.19 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(( 𝑥 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
pibt2.21 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 𝑥 ∖ Fin)∃𝑧 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
Assertion
Ref Expression
pibt2 (𝐽𝐶𝐽𝑊)
Distinct variable groups:   𝑦,𝐽,𝑥,𝑧   𝑦,𝑋,𝑥,𝑧
Allowed substitution hints:   𝐶(𝑥,𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)

Proof of Theorem pibt2
Dummy variables 𝑎 𝑏 𝑠 𝑓 𝑛 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pibt2.x . . . 4 𝑋 = 𝐽
2 pibt2.19 . . . 4 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(( 𝑥 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
31, 2pibp19 35885 . . 3 (𝐽𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
43simplbi 498 . 2 (𝐽𝐶𝐽 ∈ Top)
5 eldif 3920 . . . . 5 (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin))
6 velpw 4565 . . . . . . 7 (𝑏 ∈ 𝒫 𝑋𝑏𝑋)
76anbi1i 624 . . . . . 6 ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin))
8 vex 3449 . . . . . . . . . 10 𝑏 ∈ V
9 infinf 10502 . . . . . . . . . 10 (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏))
108, 9ax-mp 5 . . . . . . . . 9 𝑏 ∈ Fin ↔ ω ≼ 𝑏)
118infcntss 9265 . . . . . . . . 9 (ω ≼ 𝑏 → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1210, 11sylbi 216 . . . . . . . 8 𝑏 ∈ Fin → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
1312ad2antll 727 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎𝑏𝑎 ≈ ω))
14 sstr 3952 . . . . . . . . . . . . . 14 ((𝑎𝑏𝑏𝑋) → 𝑎𝑋)
1514ancoms 459 . . . . . . . . . . . . 13 ((𝑏𝑋𝑎𝑏) → 𝑎𝑋)
16 simplr 767 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω)
17 simpll 765 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽𝐶𝑎 ≈ ω))
18 0ss 4356 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∅ ⊆ 𝑎
19 sseq1 3969 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎))
2018, 19mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
2120adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
221cldlp 22501 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2322adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
2421, 23mpbird 256 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽 ∈ Top ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
254, 24sylanl1 678 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
2625adantllr 717 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
27 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅)
281cldss 22380 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ (Clsd‘𝐽) → 𝑎𝑋)
291nlpineqsn 35879 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}))
30 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → (𝑛𝑎) = {𝑝})
3130reximi 3087 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∃𝑛𝐽 (𝑛𝑎) = {𝑝})
3231ralimi 3086 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑝𝑎𝑛𝐽 (𝑝𝑛 ∧ (𝑛𝑎) = {𝑝}) → ∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝})
33 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑎 ∈ V
34 ineq1 4165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (𝑓𝑝) → (𝑛𝑎) = ((𝑓𝑝) ∩ 𝑎))
3534eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑓𝑝) → ((𝑛𝑎) = {𝑝} ↔ ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
3633, 35ac6s 10420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑝𝑎𝑛𝐽 (𝑛𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
3729, 32, 363syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
38 fvineqsnf1 35881 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎1-1𝐽)
39 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})
4038, 39jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4140eximi 1837 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑓(𝑓:𝑎𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4237, 41syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽 ∈ Top ∧ 𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
4328, 42syl3an2 1164 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
444, 43syl3an1 1163 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
45443adant1r 1177 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}))
46 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → 𝑓:𝑎1-1𝐽)
47 vsnid 4623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 𝑝 ∈ {𝑝}
48 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝}))
4947, 48mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓𝑝) ∩ 𝑎))
5049elin1d 4158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓𝑝))
5150ralimi 3086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝𝑎 𝑝 ∈ (𝑓𝑝))
52 ralssiun 35878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (∀𝑝𝑎 𝑝 ∈ (𝑓𝑝) → 𝑎 𝑝𝑎 (𝑓𝑝))
5351, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑎 𝑝𝑎 (𝑓𝑝))
5453adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 𝑝𝑎 (𝑓𝑝))
55 f1fn 6739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓:𝑎1-1𝐽𝑓 Fn 𝑎)
56 fniunfv 7194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑓 Fn 𝑎 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑓:𝑎1-1𝐽 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5857adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑝𝑎 (𝑓𝑝) = ran 𝑓)
5954, 58sseqtrd 3984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ran 𝑓)
601cldopn 22382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑎 ∈ (Clsd‘𝐽) → (𝑋𝑎) ∈ 𝐽)
6160ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋𝑎) ∈ 𝐽)
6261anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → ((𝑋𝑎) ∈ 𝐽𝑎 ran 𝑓))
6362ancomd 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))
6428ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎𝑋)
6564anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)))
66 unisng 4886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ∈ 𝐽 {(𝑋𝑎)} = (𝑋𝑎))
6766eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) = {(𝑋𝑎)})
68 eqimss 4000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) = {(𝑋𝑎)} → (𝑋𝑎) ⊆ {(𝑋𝑎)})
69 ssun4 4135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ ( ran 𝑓 {(𝑋𝑎)}))
70 uniun 4891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (ran 𝑓 ∪ {(𝑋𝑎)}) = ( ran 𝑓 {(𝑋𝑎)})
7169, 70sseqtrrdi 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑋𝑎) ⊆ {(𝑋𝑎)} → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
7267, 68, 713syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑋𝑎) ∈ 𝐽 → (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
73 ssun3 4134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑎 ran 𝑓𝑎 ⊆ ( ran 𝑓 {(𝑋𝑎)}))
7473, 70sseqtrrdi 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ran 𝑓𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}))
75 uncom 4113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎 ∪ (𝑋𝑎)) = ((𝑋𝑎) ∪ 𝑎)
76 undif1 4435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑋𝑎) ∪ 𝑎) = (𝑋𝑎)
7775, 76eqtri 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎 ∪ (𝑋𝑎)) = (𝑋𝑎)
78 ssequn2 4143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎𝑋 ↔ (𝑋𝑎) = 𝑋)
7978biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑎𝑋 → (𝑋𝑎) = 𝑋)
8077, 79eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑎𝑋 → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
8180adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) = 𝑋)
82 unss12 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})))
83 unidm 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ( (ran 𝑓 ∪ {(𝑋𝑎)}) ∪ (ran 𝑓 ∪ {(𝑋𝑎)})) = (ran 𝑓 ∪ {(𝑋𝑎)})
8482, 83sseqtrdi 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)})) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8584adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → (𝑎 ∪ (𝑋𝑎)) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
8681, 85eqsstrrd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑎𝑋 ∧ (𝑎 (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8774, 86sylanr1 680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8872, 87sylanr2 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
8988adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → 𝑋 (ran 𝑓 ∪ {(𝑋𝑎)}))
90 f1f 6738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎1-1𝐽𝑓:𝑎𝐽)
91 frn 6675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑓:𝑎𝐽 → ran 𝑓𝐽)
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑓:𝑎1-1𝐽 → ran 𝑓𝐽)
931topopn 22255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋𝐽)
941difopn 22385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝐽𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9593, 94sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋𝑎) ∈ 𝐽)
9695snssd 4769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋𝑎)} ⊆ 𝐽)
97 unss12 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ (𝐽𝐽))
98 unidm 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽𝐽) = 𝐽
9997, 98sseqtrdi 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓𝐽 ∧ {(𝑋𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
10092, 96, 99syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
101 uniss 4873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
102101, 1sseqtrrdi 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
103100, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
104103adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝑋)
10589, 104eqssd 3961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎𝑋 ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽))) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10665, 105syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ran 𝑓 ∧ (𝑋𝑎) ∈ 𝐽)) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10763, 106syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ran 𝑓) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
10859, 107sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
109108ancom1s 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
110109ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
11146, 110mpand 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
112111impr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
113112adantlrr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
1144, 113sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}))
115 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑓 ∈ V
116 f1f1orn 6795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓:𝑎1-1𝐽𝑓:𝑎1-1-onto→ran 𝑓)
117 f1oen3g 8906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ V ∧ 𝑓:𝑎1-1-onto→ran 𝑓) → 𝑎 ≈ ran 𝑓)
118115, 116, 117sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓:𝑎1-1𝐽𝑎 ≈ ran 𝑓)
119 enen1 9061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈ ω))
120 endom 8919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (ran 𝑓 ≈ ω → ran 𝑓 ≼ ω)
121 snfi 8988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 {(𝑋𝑎)} ∈ Fin
122 isfinite 9588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ({(𝑋𝑎)} ∈ Fin ↔ {(𝑋𝑎)} ≺ ω)
123121, 122mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 {(𝑋𝑎)} ≺ ω
124 sdomdom 8920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ({(𝑋𝑎)} ≺ ω → {(𝑋𝑎)} ≼ ω)
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {(𝑋𝑎)} ≼ ω
126 unctb 10141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((ran 𝑓 ≼ ω ∧ {(𝑋𝑎)} ≼ ω) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
127120, 125, 126sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (ran 𝑓 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
128119, 127syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
129118, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓:𝑎1-1𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
130129impcom 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑎 ≈ ω ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
131130adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
132131ad2ant2lr 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)
133100ancoms 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎1-1𝐽) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
134133adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
135134adantlrr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
1364, 135sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽)
137 elpw2g 5301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽))
138137biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
139138ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽))
140136, 139mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽)
1413simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
142 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑠 = 𝑧 𝑠 = 𝑧)
143142eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 = 𝑧 → (𝑋 = 𝑠𝑋 = 𝑧))
144143cbvrexvw 3226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)
145144imbi2i 335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
146145ralbii 3096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
147141, 146sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠))
148 unieq 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}))
149148eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑋 = 𝑦𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)})))
150 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω))
151149, 150anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → ((𝑋 = 𝑦𝑦 ≼ ω) ↔ (𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω)))
152 pweq 4574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
153152ineq1d 4171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin))
154153rexeqdv 3314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
155151, 154imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 = (ran 𝑓 ∪ {(𝑋𝑎)}) → (((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) ↔ ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
156155rspccv 3578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑦 ∈ 𝒫 𝐽((𝑋 = 𝑦𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑠) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
157147, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐽𝐶 → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
158157ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)))
159140, 158mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = (ran 𝑓 ∪ {(𝑋𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠))
160114, 132, 159mp2and 697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠)
161 df-rex 3074 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠))
162 elinel1 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}))
163 velpw 4565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}))
164 ssdif 4099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}))
165 difun2 4440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((ran 𝑓 ∪ {(𝑋𝑎)}) ∖ {(𝑋𝑎)}) = (ran 𝑓 ∖ {(𝑋𝑎)})
166164, 165sseqtrdi 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋𝑎)}))
167166difss2d 4094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
168163, 167sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
169162, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓)
170169a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓))
171 sseq2 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑋 = 𝑠 → (𝑎𝑋𝑎 𝑠))
172 uniexg 7677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝐽 ∈ Top → 𝐽 ∈ V)
1731, 172eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝐽 ∈ Top → 𝑋 ∈ V)
174 difexg 5284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑋 ∈ V → (𝑋𝑎) ∈ V)
175 unisng 4886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑋𝑎) ∈ V → {(𝑋𝑎)} = (𝑋𝑎))
176173, 174, 1753syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐽 ∈ Top → {(𝑋𝑎)} = (𝑋𝑎))
177176ineq2d 4172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = (𝑎 ∩ (𝑋𝑎)))
178 disjdif 4431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑎 ∩ (𝑋𝑎)) = ∅
179177, 178eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐽 ∈ Top → (𝑎 {(𝑋𝑎)}) = ∅)
180 inunissunidif 35846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑎 {(𝑋𝑎)}) = ∅ → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
181179, 180syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝐽 ∈ Top → (𝑎 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
182171, 181sylan9bbr 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
183182biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐽 ∈ Top ∧ 𝑋 = 𝑠) → (𝑎𝑋𝑎 (𝑠 ∖ {(𝑋𝑎)})))
184183impancom 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐽 ∈ Top ∧ 𝑎𝑋) → (𝑋 = 𝑠𝑎 (𝑠 ∖ {(𝑋𝑎)})))
185170, 184anim12d 609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
1864, 28, 185syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐽𝐶𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
187186adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))))
188187anim2d 612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)})))))
189118ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → 𝑎 ≈ ran 𝑓)
190 fvineqsneq 35883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑓 Fn 𝑎 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
19155, 190sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → (𝑠 ∖ {(𝑋𝑎)}) = ran 𝑓)
192 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 𝑠 ∈ V
193 difss 4091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠
194 ssdomg 8940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑠 ∈ V → ((𝑠 ∖ {(𝑋𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠))
195192, 193, 194mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∖ {(𝑋𝑎)}) ≼ 𝑠
196191, 195eqbrtrrdi 5145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → ran 𝑓𝑠)
197 endomtr 8952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑎 ≈ ran 𝑓 ∧ ran 𝑓𝑠) → 𝑎𝑠)
198189, 196, 197syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋𝑎)}) ⊆ ran 𝑓𝑎 (𝑠 ∖ {(𝑋𝑎)}))) → 𝑎𝑠)
199188, 198syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠)) → 𝑎𝑠))
200199expdimp 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑎𝑠))
201 elinel2 4156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) → 𝑠 ∈ Fin)
202201adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑠 ∈ Fin)
203202a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → 𝑠 ∈ Fin))
204200, 203jcad 513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → (𝑎𝑠𝑠 ∈ Fin)))
205204eximdv 1920 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin) ∧ 𝑋 = 𝑠) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
206161, 205biimtrid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋𝑎)}) ∩ Fin)𝑋 = 𝑠 → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
207160, 206mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
208207ex 413 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
209208exlimdv 1936 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐽𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
210209anass1rs 653 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
2112103adant3 1132 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎1-1𝐽 ∧ ∀𝑝𝑎 ((𝑓𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin)))
21245, 211mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
21317, 26, 27, 212syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
214213anasss 467 . . . . . . . . . . . . . . . . . . 19 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎𝑠𝑠 ∈ Fin))
215 isfinite 9588 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ Fin ↔ 𝑠 ≺ ω)
216 domsdomtr 9056 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎𝑠𝑠 ≺ ω) → 𝑎 ≺ ω)
217215, 216sylan2b 594 . . . . . . . . . . . . . . . . . . . 20 ((𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
218217exlimiv 1933 . . . . . . . . . . . . . . . . . . 19 (∃𝑠(𝑎𝑠𝑠 ∈ Fin) → 𝑎 ≺ ω)
219 sdomnen 8921 . . . . . . . . . . . . . . . . . . 19 (𝑎 ≺ ω → ¬ 𝑎 ≈ ω)
220214, 218, 2193syl 18 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω)
22116, 220pm2.65da 815 . . . . . . . . . . . . . . . . 17 ((𝐽𝐶𝑎 ≈ ω) → ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
222 imnan 400 . . . . . . . . . . . . . . . . 17 ((𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
223221, 222sylibr 233 . . . . . . . . . . . . . . . 16 ((𝐽𝐶𝑎 ≈ ω) → (𝑎𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅))
224223imp 407 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅)
225 neq0 4305 . . . . . . . . . . . . . . 15 (¬ ((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
226224, 225sylib 217 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2271lpss 22493 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Top ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
2284, 227sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝐽𝐶𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
229228adantlr 713 . . . . . . . . . . . . . . . . . 18 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
230229sseld 3943 . . . . . . . . . . . . . . . . 17 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠𝑋))
231230ancrd 552 . . . . . . . . . . . . . . . 16 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
232231eximdv 1920 . . . . . . . . . . . . . . 15 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
233 df-rex 3074 . . . . . . . . . . . . . . 15 (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠𝑋𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
234232, 233syl6ibr 251 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
235226, 234mpd 15 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ 𝑎𝑋) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
23615, 235sylan2 593 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
2371lpss3 22495 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑏𝑋𝑎𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2382373expb 1120 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
2394, 238sylan 580 . . . . . . . . . . . . . . 15 ((𝐽𝐶 ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
240239adantlr 713 . . . . . . . . . . . . . 14 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
241240sseld 3943 . . . . . . . . . . . . 13 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
242241reximdv 3167 . . . . . . . . . . . 12 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → (∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
243236, 242mpd 15 . . . . . . . . . . 11 (((𝐽𝐶𝑎 ≈ ω) ∧ (𝑏𝑋𝑎𝑏)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
244243an42s 659 . . . . . . . . . 10 (((𝐽𝐶𝑏𝑋) ∧ (𝑎𝑏𝑎 ≈ ω)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
245244ex 413 . . . . . . . . 9 ((𝐽𝐶𝑏𝑋) → ((𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
246245exlimdv 1936 . . . . . . . 8 ((𝐽𝐶𝑏𝑋) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
247246adantrr 715 . . . . . . 7 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎𝑏𝑎 ≈ ω) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
24813, 247mpd 15 . . . . . 6 ((𝐽𝐶 ∧ (𝑏𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2497, 248sylan2b 594 . . . . 5 ((𝐽𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
2505, 249sylan2b 594 . . . 4 ((𝐽𝐶𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
251250ralrimiva 3143 . . 3 (𝐽𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
252 simpr 485 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → 𝑧 = 𝑠)
253 fveq2 6842 . . . . . . 7 (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
254253adantr 481 . . . . . 6 ((𝑦 = 𝑏𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
255252, 254eleq12d 2832 . . . . 5 ((𝑦 = 𝑏𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
256255cbvrexdva 3327 . . . 4 (𝑦 = 𝑏 → (∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
257256cbvralvw 3225 . . 3 (∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
258251, 257sylibr 233 . 2 (𝐽𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))
259 pibt2.21 . . 3 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 𝑥 ∖ Fin)∃𝑧 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
2601, 259pibp21 35886 . 2 (𝐽𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)))
2614, 258, 260sylanbrc 583 1 (𝐽𝐶𝐽𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   cuni 4865   ciun 4954   class class class wbr 5105  ran crn 5634   Fn wfn 6491  wf 6492  1-1wf1 6493  1-1-ontowf1o 6495  cfv 6496  ωcom 7802  cen 8880  cdom 8881  csdm 8882  Fincfn 8883  Topctop 22242  Clsdccld 22367  limPtclp 22485
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-reg 9528  ax-inf2 9577  ax-ac2 10399
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-oi 9446  df-r1 9700  df-rank 9701  df-dju 9837  df-card 9875  df-ac 10052  df-top 22243  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator