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