Metamath Proof Explorer

Theorem pibt2

Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 and pibp21 for the definitions of the relevant properties. This proof uses the axiom of choice. (Contributed by ML, 30-Mar-2021)

Ref Expression
Hypotheses pibt2.x ⊢ 𝑋 = ∪ 𝐽
pibt2.19 ⊢ 𝐶 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }
pibt2.21 ⊢ 𝑊 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∖ Fin ) ∃ 𝑧 ∈ ∪ 𝑥 𝑧 ∈ ( ( limPt ‘ 𝑥 ) ‘ 𝑦 ) }
Assertion pibt2 ( 𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊 )

Proof

Step Hyp Ref Expression
1 pibt2.x ⊢ 𝑋 = ∪ 𝐽
2 pibt2.19 ⊢ 𝐶 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }
3 pibt2.21 ⊢ 𝑊 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ ( 𝒫 ∪ 𝑥 ∖ Fin ) ∃ 𝑧 ∈ ∪ 𝑥 𝑧 ∈ ( ( limPt ‘ 𝑥 ) ‘ 𝑦 ) }
4 1 2 pibp19 ⊢ ( 𝐽 ∈ 𝐶 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
5 4 simplbi ⊢ ( 𝐽 ∈ 𝐶 → 𝐽 ∈ Top )
6 eldif ⊢ ( 𝑏 ∈ ( 𝒫 𝑋 ∖ Fin ) ↔ ( 𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin ) )
7 velpw ⊢ ( 𝑏 ∈ 𝒫 𝑋 ↔ 𝑏 ⊆ 𝑋 )
8 7 anbi1i ⊢ ( ( 𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin ) ↔ ( 𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin ) )
9 vex ⊢ 𝑏 ∈ V
10 infinf ⊢ ( 𝑏 ∈ V → ( ¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏 ) )
11 9 10 ax-mp ⊢ ( ¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏 )
12 9 infcntss ⊢ ( ω ≼ 𝑏 → ∃ 𝑎 ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) )
13 11 12 sylbi ⊢ ( ¬ 𝑏 ∈ Fin → ∃ 𝑎 ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) )
14 13 ad2antll ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin ) ) → ∃ 𝑎 ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) )
15 sstr ⊢ ( ( 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) → 𝑎 ⊆ 𝑋 )
16 15 ancoms ⊢ ( ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) → 𝑎 ⊆ 𝑋 )
17 simplr ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) ) → 𝑎 ≈ ω )
18 simpll ⊢ ( ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) )
19 0ss ⊢ ∅ ⊆ 𝑎
20 sseq1 ⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ → ( ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎 ) )
21 19 20 mpbiri ⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑎 )
22 21 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑎 )
23 1 cldlp ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) → ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑎 ) )
24 23 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑎 ) )
25 22 24 mpbird ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → 𝑎 ∈ ( Clsd ‘ 𝐽 ) )
26 5 25 sylanl1 ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → 𝑎 ∈ ( Clsd ‘ 𝐽 ) )
27 26 adantllr ⊢ ( ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → 𝑎 ∈ ( Clsd ‘ 𝐽 ) )
28 simpr ⊢ ( ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ )
29 1 cldss ⊢ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) → 𝑎 ⊆ 𝑋 )
30 1 nlpineqsn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∀ 𝑝 ∈ 𝑎 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ) )
31 simpr ⊢ ( ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ) → ( 𝑛 ∩ 𝑎 ) = { 𝑝 } )
32 31 reximi ⊢ ( ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝑎 ) = { 𝑝 } )
33 32 ralimi ⊢ ( ∀ 𝑝 ∈ 𝑎 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ) → ∀ 𝑝 ∈ 𝑎 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝑎 ) = { 𝑝 } )
34 vex ⊢ 𝑎 ∈ V
35 ineq1 ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑝 ) → ( 𝑛 ∩ 𝑎 ) = ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) )
36 35 eqeq1d ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑝 ) → ( ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ↔ ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
37 34 36 ac6s ⊢ ( ∀ 𝑝 ∈ 𝑎 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝑎 ) = { 𝑝 } → ∃ 𝑓 ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
38 30 33 37 3syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
39 fvineqsnf1 ⊢ ( ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → 𝑓 : 𝑎 –1-1→ 𝐽 )
40 simpr ⊢ ( ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } )
41 39 40 jca ⊢ ( ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
42 41 eximi ⊢ ( ∃ 𝑓 ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
43 38 42 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
44 29 43 syl3an2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
45 5 44 syl3an1 ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
46 45 3adant1r ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
47 simpr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) → 𝑓 : 𝑎 –1-1→ 𝐽 )
48 vsnid ⊢ 𝑝 ∈ { 𝑝 }
49 eleq2 ⊢ ( ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → ( 𝑝 ∈ ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) ↔ 𝑝 ∈ { 𝑝 } ) )
50 48 49 mpbiri ⊢ ( ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → 𝑝 ∈ ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) )
51 50 elin1d ⊢ ( ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → 𝑝 ∈ ( 𝑓 ‘ 𝑝 ) )
52 51 ralimi ⊢ ( ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → ∀ 𝑝 ∈ 𝑎 𝑝 ∈ ( 𝑓 ‘ 𝑝 ) )
53 ralssiun ⊢ ( ∀ 𝑝 ∈ 𝑎 𝑝 ∈ ( 𝑓 ‘ 𝑝 ) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) )
54 52 53 syl ⊢ ( ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) )
55 54 adantl ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) )
56 f1fn ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → 𝑓 Fn 𝑎 )
57 fniunfv ⊢ ( 𝑓 Fn 𝑎 → ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) = ∪ ran 𝑓 )
58 56 57 syl ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) = ∪ ran 𝑓 )
59 58 adantr ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) = ∪ ran 𝑓 )
60 55 59 sseqtrd ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → 𝑎 ⊆ ∪ ran 𝑓 )
61 1 cldopn ⊢ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 )
62 61 ad2antll ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 )
63 62 anim1i ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ 𝑎 ⊆ ∪ ran 𝑓 ) → ( ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ∧ 𝑎 ⊆ ∪ ran 𝑓 ) )
64 63 ancomd ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ 𝑎 ⊆ ∪ ran 𝑓 ) → ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) )
65 29 ad2antll ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) → 𝑎 ⊆ 𝑋 )
66 65 anim1i ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) → ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) )
67 unisng ⊢ ( ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 → ∪ { ( 𝑋 ∖ 𝑎 ) } = ( 𝑋 ∖ 𝑎 ) )
68 67 eqcomd ⊢ ( ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 → ( 𝑋 ∖ 𝑎 ) = ∪ { ( 𝑋 ∖ 𝑎 ) } )
69 eqimss ⊢ ( ( 𝑋 ∖ 𝑎 ) = ∪ { ( 𝑋 ∖ 𝑎 ) } → ( 𝑋 ∖ 𝑎 ) ⊆ ∪ { ( 𝑋 ∖ 𝑎 ) } )
70 ssun4 ⊢ ( ( 𝑋 ∖ 𝑎 ) ⊆ ∪ { ( 𝑋 ∖ 𝑎 ) } → ( 𝑋 ∖ 𝑎 ) ⊆ ( ∪ ran 𝑓 ∪ ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
71 uniun ⊢ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) = ( ∪ ran 𝑓 ∪ ∪ { ( 𝑋 ∖ 𝑎 ) } )
72 70 71 sseqtrrdi ⊢ ( ( 𝑋 ∖ 𝑎 ) ⊆ ∪ { ( 𝑋 ∖ 𝑎 ) } → ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
73 68 69 72 3syl ⊢ ( ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 → ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
74 ssun3 ⊢ ( 𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ ( ∪ ran 𝑓 ∪ ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
75 74 71 sseqtrrdi ⊢ ( 𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
76 uncom ⊢ ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) = ( ( 𝑋 ∖ 𝑎 ) ∪ 𝑎 )
77 undif1 ⊢ ( ( 𝑋 ∖ 𝑎 ) ∪ 𝑎 ) = ( 𝑋 ∪ 𝑎 )
78 76 77 eqtri ⊢ ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) = ( 𝑋 ∪ 𝑎 )
79 ssequn2 ⊢ ( 𝑎 ⊆ 𝑋 ↔ ( 𝑋 ∪ 𝑎 ) = 𝑋 )
80 79 biimpi ⊢ ( 𝑎 ⊆ 𝑋 → ( 𝑋 ∪ 𝑎 ) = 𝑋 )
81 78 80 syl5eq ⊢ ( 𝑎 ⊆ 𝑋 → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) = 𝑋 )
82 81 adantr ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) = 𝑋 )
83 unss12 ⊢ ( ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) ⊆ ( ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∪ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) )
84 unidm ⊢ ( ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∪ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } )
85 83 84 sseqtrdi ⊢ ( ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
86 85 adantl ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
87 82 86 eqsstrrd ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
88 75 87 sylanr1 ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
89 73 88 sylanr2 ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
90 89 adantl ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
91 f1f ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → 𝑓 : 𝑎 ⟶ 𝐽 )
92 frn ⊢ ( 𝑓 : 𝑎 ⟶ 𝐽 → ran 𝑓 ⊆ 𝐽 )
93 91 92 syl ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → ran 𝑓 ⊆ 𝐽 )
94 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
95 1 difopn ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 )
96 94 95 sylan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 )
97 96 snssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → { ( 𝑋 ∖ 𝑎 ) } ⊆ 𝐽 )
98 unss12 ⊢ ( ( ran 𝑓 ⊆ 𝐽 ∧ { ( 𝑋 ∖ 𝑎 ) } ⊆ 𝐽 ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ( 𝐽 ∪ 𝐽 ) )
99 unidm ⊢ ( 𝐽 ∪ 𝐽 ) = 𝐽
100 98 99 sseqtrdi ⊢ ( ( ran 𝑓 ⊆ 𝐽 ∧ { ( 𝑋 ∖ 𝑎 ) } ⊆ 𝐽 ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 )
101 93 97 100 syl2an ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 )
102 uniss ⊢ ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 → ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ∪ 𝐽 )
103 102 1 sseqtrrdi ⊢ ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 → ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑋 )
104 101 103 syl ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) → ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑋 )
105 104 adantr ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) ) → ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑋 )
106 90 105 eqssd ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
107 66 106 syldan ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
108 64 107 syldan ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ 𝑎 ⊆ ∪ ran 𝑓 ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
109 60 108 sylan2 ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
110 109 ancom1s ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
111 110 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) → ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) )
112 47 111 mpand ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) → ( ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) )
113 112 impr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
114 113 adantlrr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
115 5 114 sylanl1 ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
116 vex ⊢ 𝑓 ∈ V
117 f1f1orn ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → 𝑓 : 𝑎 –1-1-onto→ ran 𝑓 )
118 f1oen3g ⊢ ( ( 𝑓 ∈ V ∧ 𝑓 : 𝑎 –1-1-onto→ ran 𝑓 ) → 𝑎 ≈ ran 𝑓 )
119 116 117 118 sylancr ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → 𝑎 ≈ ran 𝑓 )
120 enen1 ⊢ ( 𝑎 ≈ ran 𝑓 → ( 𝑎 ≈ ω ↔ ran 𝑓 ≈ ω ) )
121 endom ⊢ ( ran 𝑓 ≈ ω → ran 𝑓 ≼ ω )
122 snfi ⊢ { ( 𝑋 ∖ 𝑎 ) } ∈ Fin
123 isfinite ⊢ ( { ( 𝑋 ∖ 𝑎 ) } ∈ Fin ↔ { ( 𝑋 ∖ 𝑎 ) } ≺ ω )
124 122 123 mpbi ⊢ { ( 𝑋 ∖ 𝑎 ) } ≺ ω
125 sdomdom ⊢ ( { ( 𝑋 ∖ 𝑎 ) } ≺ ω → { ( 𝑋 ∖ 𝑎 ) } ≼ ω )
126 124 125 ax-mp ⊢ { ( 𝑋 ∖ 𝑎 ) } ≼ ω
127 unctb ⊢ ( ( ran 𝑓 ≼ ω ∧ { ( 𝑋 ∖ 𝑎 ) } ≼ ω ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω )
128 121 126 127 sylancl ⊢ ( ran 𝑓 ≈ ω → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω )
129 120 128 syl6bi ⊢ ( 𝑎 ≈ ran 𝑓 → ( 𝑎 ≈ ω → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) )
130 119 129 syl ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → ( 𝑎 ≈ ω → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) )
131 130 impcom ⊢ ( ( 𝑎 ≈ ω ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω )
132 131 adantll ⊢ ( ( ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω )
133 132 ad2ant2lr ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω )
134 101 ancoms ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 )
135 134 adantrr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 )
136 135 adantlrr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 )
137 5 136 sylanl1 ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 )
138 elpw2g ⊢ ( 𝐽 ∈ 𝐶 → ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∈ 𝒫 𝐽 ↔ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 ) )
139 138 biimprd ⊢ ( 𝐽 ∈ 𝐶 → ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∈ 𝒫 𝐽 ) )
140 139 ad2antrr ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∈ 𝒫 𝐽 ) )
141 137 140 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∈ 𝒫 𝐽 )
142 4 simprbi ⊢ ( 𝐽 ∈ 𝐶 → ∀ 𝑦 ∈ 𝒫 𝐽 ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
143 unieq ⊢ ( 𝑠 = 𝑧 → ∪ 𝑠 = ∪ 𝑧 )
144 143 eqeq2d ⊢ ( 𝑠 = 𝑧 → ( 𝑋 = ∪ 𝑠 ↔ 𝑋 = ∪ 𝑧 ) )
145 144 cbvrexvw ⊢ ( ∃ 𝑠 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑠 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 )
146 145 imbi2i ⊢ ( ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑠 ) ↔ ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
147 146 ralbii ⊢ ( ∀ 𝑦 ∈ 𝒫 𝐽 ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑠 ) ↔ ∀ 𝑦 ∈ 𝒫 𝐽 ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
148 142 147 sylibr ⊢ ( 𝐽 ∈ 𝐶 → ∀ 𝑦 ∈ 𝒫 𝐽 ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
149 unieq ⊢ ( 𝑦 = ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ∪ 𝑦 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
150 149 eqeq2d ⊢ ( 𝑦 = ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( 𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) )
151 breq1 ⊢ ( 𝑦 = ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( 𝑦 ≼ ω ↔ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) )
152 150 151 anbi12d ⊢ ( 𝑦 = ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) ↔ ( 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) ) )
153 pweq ⊢ ( 𝑦 = ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → 𝒫 𝑦 = 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
154 153 ineq1d ⊢ ( 𝑦 = ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( 𝒫 𝑦 ∩ Fin ) = ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) )
155 154 rexeqdv ⊢ ( 𝑦 = ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( ∃ 𝑠 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑠 ↔ ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
156 152 155 imbi12d ⊢ ( 𝑦 = ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑠 ) ↔ ( ( 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 ) ) )
157 156 rspccv ⊢ ( ∀ 𝑦 ∈ 𝒫 𝐽 ( ( 𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑠 ) → ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∈ 𝒫 𝐽 → ( ( 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 ) ) )
158 148 157 syl ⊢ ( 𝐽 ∈ 𝐶 → ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∈ 𝒫 𝐽 → ( ( 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 ) ) )
159 158 ad2antrr ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∈ 𝒫 𝐽 → ( ( 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 ) ) )
160 141 159 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ( 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) → ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 ) )
161 115 133 160 mp2and ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 )
162 df-rex ⊢ ( ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 ↔ ∃ 𝑠 ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) )
163 elinel1 ⊢ ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) → 𝑠 ∈ 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
164 velpw ⊢ ( 𝑠 ∈ 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ↔ 𝑠 ⊆ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
165 ssdif ⊢ ( 𝑠 ⊆ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∖ { ( 𝑋 ∖ 𝑎 ) } ) )
166 difun2 ⊢ ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∖ { ( 𝑋 ∖ 𝑎 ) } ) = ( ran 𝑓 ∖ { ( 𝑋 ∖ 𝑎 ) } )
167 165 166 sseqtrdi ⊢ ( 𝑠 ⊆ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ( ran 𝑓 ∖ { ( 𝑋 ∖ 𝑎 ) } ) )
168 167 difss2d ⊢ ( 𝑠 ⊆ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 )
169 164 168 sylbi ⊢ ( 𝑠 ∈ 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 )
170 163 169 syl ⊢ ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 )
171 170 a1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) → ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ) )
172 sseq2 ⊢ ( 𝑋 = ∪ 𝑠 → ( 𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ 𝑠 ) )
173 uniexg ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V )
174 1 173 eqeltrid ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ V )
175 difexg ⊢ ( 𝑋 ∈ V → ( 𝑋 ∖ 𝑎 ) ∈ V )
176 unisng ⊢ ( ( 𝑋 ∖ 𝑎 ) ∈ V → ∪ { ( 𝑋 ∖ 𝑎 ) } = ( 𝑋 ∖ 𝑎 ) )
177 174 175 176 3syl ⊢ ( 𝐽 ∈ Top → ∪ { ( 𝑋 ∖ 𝑎 ) } = ( 𝑋 ∖ 𝑎 ) )
178 177 ineq2d ⊢ ( 𝐽 ∈ Top → ( 𝑎 ∩ ∪ { ( 𝑋 ∖ 𝑎 ) } ) = ( 𝑎 ∩ ( 𝑋 ∖ 𝑎 ) ) )
179 disjdif ⊢ ( 𝑎 ∩ ( 𝑋 ∖ 𝑎 ) ) = ∅
180 178 179 eqtrdi ⊢ ( 𝐽 ∈ Top → ( 𝑎 ∩ ∪ { ( 𝑋 ∖ 𝑎 ) } ) = ∅ )
181 inunissunidif ⊢ ( ( 𝑎 ∩ ∪ { ( 𝑋 ∖ 𝑎 ) } ) = ∅ → ( 𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
182 180 181 syl ⊢ ( 𝐽 ∈ Top → ( 𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
183 172 182 sylan9bbr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠 ) → ( 𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
184 183 biimpd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠 ) → ( 𝑎 ⊆ 𝑋 → 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
185 184 impancom ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) → ( 𝑋 = ∪ 𝑠 → 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
186 171 185 anim12d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) )
187 5 29 186 syl2an ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) )
188 187 adantrr ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) )
189 188 anim2d ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) ) → ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) ) )
190 119 ad2antrr ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → 𝑎 ≈ ran 𝑓 )
191 fvineqsneq ⊢ ( ( ( 𝑓 Fn 𝑎 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) = ran 𝑓 )
192 56 191 sylanl1 ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) = ran 𝑓 )
193 vex ⊢ 𝑠 ∈ V
194 difss ⊢ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑠
195 ssdomg ⊢ ( 𝑠 ∈ V → ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑠 → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ≼ 𝑠 ) )
196 193 194 195 mp2 ⊢ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ≼ 𝑠
197 192 196 eqbrtrrdi ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ran 𝑓 ≼ 𝑠 )
198 endomtr ⊢ ( ( 𝑎 ≈ ran 𝑓 ∧ ran 𝑓 ≼ 𝑠 ) → 𝑎 ≼ 𝑠 )
199 190 197 198 syl2anc ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → 𝑎 ≼ 𝑠 )
200 189 199 syl6 ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) ) → 𝑎 ≼ 𝑠 ) )
201 200 expdimp ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → 𝑎 ≼ 𝑠 ) )
202 elinel2 ⊢ ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) → 𝑠 ∈ Fin )
203 202 adantr ⊢ ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → 𝑠 ∈ Fin )
204 203 a1i ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → 𝑠 ∈ Fin ) )
205 201 204 jcad ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
206 205 eximdv ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ∃ 𝑠 ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
207 162 206 syl5bi ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
208 161 207 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) )
209 208 ex ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
210 209 exlimdv ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
211 210 anass1rs ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
212 211 3adant3 ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ( ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
213 46 212 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) )
214 18 27 28 213 syl3anc ⊢ ( ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) )
215 214 anasss ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) )
216 isfinite ⊢ ( 𝑠 ∈ Fin ↔ 𝑠 ≺ ω )
217 domsdomtr ⊢ ( ( 𝑎 ≼ 𝑠 ∧ 𝑠 ≺ ω ) → 𝑎 ≺ ω )
218 216 217 sylan2b ⊢ ( ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) → 𝑎 ≺ ω )
219 218 exlimiv ⊢ ( ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) → 𝑎 ≺ ω )
220 sdomnen ⊢ ( 𝑎 ≺ ω → ¬ 𝑎 ≈ ω )
221 215 219 220 3syl ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) ) → ¬ 𝑎 ≈ ω )
222 17 221 pm2.65da ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) → ¬ ( 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) )
223 imnan ⊢ ( ( 𝑎 ⊆ 𝑋 → ¬ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) ↔ ¬ ( 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) )
224 222 223 sylibr ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) → ( 𝑎 ⊆ 𝑋 → ¬ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) )
225 224 imp ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ¬ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ )
226 neq0 ⊢ ( ¬ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ↔ ∃ 𝑠 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) )
227 225 226 sylib ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ∃ 𝑠 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) )
228 1 lpss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑋 )
229 5 228 sylan ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑋 )
230 229 adantlr ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑋 )
231 230 sseld ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → 𝑠 ∈ 𝑋 ) )
232 231 ancrd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → ( 𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ) ) )
233 232 eximdv ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( ∃ 𝑠 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ) ) )
234 df-rex ⊢ ( ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ) )
235 233 234 syl6ibr ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( ∃ 𝑠 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ) )
236 227 235 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) )
237 16 236 sylan2 ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) )
238 1 lpss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
239 238 3expb ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
240 5 239 sylan ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
241 240 adantlr ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
242 241 sseld ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
243 242 reximdv ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
244 237 243 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
245 244 an42s ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋 ) ∧ ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
246 245 ex ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋 ) → ( ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
247 246 exlimdv ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋 ) → ( ∃ 𝑎 ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
248 247 adantrr ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin ) ) → ( ∃ 𝑎 ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
249 14 248 mpd ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
250 8 249 sylan2b ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
251 6 250 sylan2b ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑏 ∈ ( 𝒫 𝑋 ∖ Fin ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
252 251 ralrimiva ⊢ ( 𝐽 ∈ 𝐶 → ∀ 𝑏 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
253 simpr ⊢ ( ( 𝑦 = 𝑏 ∧ 𝑧 = 𝑠 ) → 𝑧 = 𝑠 )
254 fveq2 ⊢ ( 𝑦 = 𝑏 → ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
255 254 adantr ⊢ ( ( 𝑦 = 𝑏 ∧ 𝑧 = 𝑠 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
256 253 255 eleq12d ⊢ ( ( 𝑦 = 𝑏 ∧ 𝑧 = 𝑠 ) → ( 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ↔ 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
257 256 cbvrexdva ⊢ ( 𝑦 = 𝑏 → ( ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ↔ ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
258 257 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
259 252 258 sylibr ⊢ ( 𝐽 ∈ 𝐶 → ∀ 𝑦 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) )
260 1 3 pibp21 ⊢ ( 𝐽 ∈ 𝑊 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ) )
261 5 259 260 sylanbrc ⊢ ( 𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊 )