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) Remove dependency on ax-reg . (Revised by Timothy J. O'Malley, 15-Oct-2026)

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 infinf ⊢ ( 𝑏 ∈ V → ( ¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏 ) )
10 9 elv ⊢ ( ¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏 )
11 vex ⊢ 𝑏 ∈ V
12 11 infcntss ⊢ ( ω ≼ 𝑏 → ∃ 𝑎 ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) )
13 10 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 vex ⊢ 𝑎 ∈ V
31 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → 𝐽 ∈ Top )
32 31 elexd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → 𝐽 ∈ V )
33 1 nlpineqsn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∀ 𝑝 ∈ 𝑎 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ) )
34 simpr ⊢ ( ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ) → ( 𝑛 ∩ 𝑎 ) = { 𝑝 } )
35 34 reximi ⊢ ( ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝑎 ) = { 𝑝 } )
36 35 ralimi ⊢ ( ∀ 𝑝 ∈ 𝑎 ∃ 𝑛 ∈ 𝐽 ( 𝑝 ∈ 𝑛 ∧ ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ) → ∀ 𝑝 ∈ 𝑎 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝑎 ) = { 𝑝 } )
37 33 36 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∀ 𝑝 ∈ 𝑎 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝑎 ) = { 𝑝 } )
38 ineq1 ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑝 ) → ( 𝑛 ∩ 𝑎 ) = ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) )
39 38 eqeq1d ⊢ ( 𝑛 = ( 𝑓 ‘ 𝑝 ) → ( ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ↔ ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
40 39 ac6 ⊢ ( ( 𝑎 ∈ V ∧ 𝐽 ∈ V ∧ ∀ 𝑝 ∈ 𝑎 ∃ 𝑛 ∈ 𝐽 ( 𝑛 ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑓 ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
41 30 32 37 40 mp3an2i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
42 fvineqsnf1 ⊢ ( ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → 𝑓 : 𝑎 –1-1→ 𝐽 )
43 simpr ⊢ ( ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } )
44 42 43 jca ⊢ ( ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
45 44 eximi ⊢ ( ∃ 𝑓 ( 𝑓 : 𝑎 ⟶ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
46 41 45 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
47 29 46 syl3an2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
48 5 47 syl3an1 ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
49 48 3adant1r ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) )
50 simpr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) → 𝑓 : 𝑎 –1-1→ 𝐽 )
51 vsnid ⊢ 𝑝 ∈ { 𝑝 }
52 eleq2 ⊢ ( ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → ( 𝑝 ∈ ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) ↔ 𝑝 ∈ { 𝑝 } ) )
53 51 52 mpbiri ⊢ ( ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → 𝑝 ∈ ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) )
54 53 elin1d ⊢ ( ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → 𝑝 ∈ ( 𝑓 ‘ 𝑝 ) )
55 54 ralimi ⊢ ( ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → ∀ 𝑝 ∈ 𝑎 𝑝 ∈ ( 𝑓 ‘ 𝑝 ) )
56 ralssiun ⊢ ( ∀ 𝑝 ∈ 𝑎 𝑝 ∈ ( 𝑓 ‘ 𝑝 ) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) )
57 55 56 syl ⊢ ( ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) )
58 57 adantl ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) )
59 f1fn ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → 𝑓 Fn 𝑎 )
60 fniunfv ⊢ ( 𝑓 Fn 𝑎 → ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) = ∪ ran 𝑓 )
61 59 60 syl ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) = ∪ ran 𝑓 )
62 61 adantr ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∪ 𝑝 ∈ 𝑎 ( 𝑓 ‘ 𝑝 ) = ∪ ran 𝑓 )
63 58 62 sseqtrd ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → 𝑎 ⊆ ∪ ran 𝑓 )
64 1 cldopn ⊢ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 )
65 64 ad2antll ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 )
66 65 anim1ci ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ 𝑎 ⊆ ∪ ran 𝑓 ) → ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) )
67 29 ad2antll ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) → 𝑎 ⊆ 𝑋 )
68 67 anim1i ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) → ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) )
69 unisng ⊢ ( ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 → ∪ { ( 𝑋 ∖ 𝑎 ) } = ( 𝑋 ∖ 𝑎 ) )
70 69 eqcomd ⊢ ( ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 → ( 𝑋 ∖ 𝑎 ) = ∪ { ( 𝑋 ∖ 𝑎 ) } )
71 eqimss ⊢ ( ( 𝑋 ∖ 𝑎 ) = ∪ { ( 𝑋 ∖ 𝑎 ) } → ( 𝑋 ∖ 𝑎 ) ⊆ ∪ { ( 𝑋 ∖ 𝑎 ) } )
72 ssun4 ⊢ ( ( 𝑋 ∖ 𝑎 ) ⊆ ∪ { ( 𝑋 ∖ 𝑎 ) } → ( 𝑋 ∖ 𝑎 ) ⊆ ( ∪ ran 𝑓 ∪ ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
73 uniun ⊢ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) = ( ∪ ran 𝑓 ∪ ∪ { ( 𝑋 ∖ 𝑎 ) } )
74 72 73 sseqtrrdi ⊢ ( ( 𝑋 ∖ 𝑎 ) ⊆ ∪ { ( 𝑋 ∖ 𝑎 ) } → ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
75 70 71 74 3syl ⊢ ( ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 → ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
76 ssun3 ⊢ ( 𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ ( ∪ ran 𝑓 ∪ ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
77 76 73 sseqtrrdi ⊢ ( 𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
78 uncom ⊢ ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) = ( ( 𝑋 ∖ 𝑎 ) ∪ 𝑎 )
79 undif1 ⊢ ( ( 𝑋 ∖ 𝑎 ) ∪ 𝑎 ) = ( 𝑋 ∪ 𝑎 )
80 78 79 eqtri ⊢ ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) = ( 𝑋 ∪ 𝑎 )
81 ssequn2 ⊢ ( 𝑎 ⊆ 𝑋 ↔ ( 𝑋 ∪ 𝑎 ) = 𝑋 )
82 81 biimpi ⊢ ( 𝑎 ⊆ 𝑋 → ( 𝑋 ∪ 𝑎 ) = 𝑋 )
83 80 82 eqtrid ⊢ ( 𝑎 ⊆ 𝑋 → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) = 𝑋 )
84 83 adantr ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) = 𝑋 )
85 unss12 ⊢ ( ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) ⊆ ( ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∪ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) )
86 unidm ⊢ ( ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∪ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } )
87 85 86 sseqtrdi ⊢ ( ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
88 87 adantl ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ( 𝑎 ∪ ( 𝑋 ∖ 𝑎 ) ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
89 84 88 eqsstrrd ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
90 77 89 sylanr1 ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
91 75 90 sylanr2 ⊢ ( ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
92 91 adantl ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
93 f1f ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → 𝑓 : 𝑎 ⟶ 𝐽 )
94 93 frnd ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → ran 𝑓 ⊆ 𝐽 )
95 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
96 1 difopn ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 )
97 95 96 sylan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 )
98 97 snssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → { ( 𝑋 ∖ 𝑎 ) } ⊆ 𝐽 )
99 unss12 ⊢ ( ( ran 𝑓 ⊆ 𝐽 ∧ { ( 𝑋 ∖ 𝑎 ) } ⊆ 𝐽 ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ( 𝐽 ∪ 𝐽 ) )
100 unidm ⊢ ( 𝐽 ∪ 𝐽 ) = 𝐽
101 99 100 sseqtrdi ⊢ ( ( ran 𝑓 ⊆ 𝐽 ∧ { ( 𝑋 ∖ 𝑎 ) } ⊆ 𝐽 ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 )
102 94 98 101 syl2an ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 )
103 uniss ⊢ ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 → ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ∪ 𝐽 )
104 103 1 sseqtrrdi ⊢ ( ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝐽 → ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑋 )
105 102 104 syl ⊢ ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) → ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑋 )
106 105 adantr ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) ) → ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑋 )
107 92 106 eqssd ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
108 68 107 syldan ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑎 ⊆ ∪ ran 𝑓 ∧ ( 𝑋 ∖ 𝑎 ) ∈ 𝐽 ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
109 66 108 syldan ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ 𝑎 ⊆ ∪ ran 𝑓 ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
110 63 109 sylan2 ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
111 110 ancom1s ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
112 111 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) → ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) )
113 50 112 mpand ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 : 𝑎 –1-1→ 𝐽 ) → ( ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ) )
114 113 impr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
115 114 adantlrr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
116 5 115 sylanl1 ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) )
117 vex ⊢ 𝑓 ∈ V
118 f1f1orn ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → 𝑓 : 𝑎 –1-1-onto→ ran 𝑓 )
119 f1oen3g ⊢ ( ( 𝑓 ∈ V ∧ 𝑓 : 𝑎 –1-1-onto→ ran 𝑓 ) → 𝑎 ≈ ran 𝑓 )
120 117 118 119 sylancr ⊢ ( 𝑓 : 𝑎 –1-1→ 𝐽 → 𝑎 ≈ ran 𝑓 )
121 enen1 ⊢ ( 𝑎 ≈ ran 𝑓 → ( 𝑎 ≈ ω ↔ ran 𝑓 ≈ ω ) )
122 endom ⊢ ( ran 𝑓 ≈ ω → ran 𝑓 ≼ ω )
123 snfi ⊢ { ( 𝑋 ∖ 𝑎 ) } ∈ Fin
124 fict ⊢ ( { ( 𝑋 ∖ 𝑎 ) } ∈ Fin → { ( 𝑋 ∖ 𝑎 ) } ≼ ω )
125 123 124 ax-mp ⊢ { ( 𝑋 ∖ 𝑎 ) } ≼ ω
126 unctb ⊢ ( ( ran 𝑓 ≼ ω ∧ { ( 𝑋 ∖ 𝑎 ) } ≼ ω ) → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω )
127 122 125 126 sylancl ⊢ ( ran 𝑓 ≈ ω → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω )
128 121 127 biimtrdi ⊢ ( 𝑎 ≈ ran 𝑓 → ( 𝑎 ≈ ω → ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ≼ ω ) )
129 120 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 102 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 116 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 95 elexd ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ V )
173 difexg ⊢ ( 𝑋 ∈ V → ( 𝑋 ∖ 𝑎 ) ∈ V )
174 unisng ⊢ ( ( 𝑋 ∖ 𝑎 ) ∈ V → ∪ { ( 𝑋 ∖ 𝑎 ) } = ( 𝑋 ∖ 𝑎 ) )
175 172 173 174 3syl ⊢ ( 𝐽 ∈ Top → ∪ { ( 𝑋 ∖ 𝑎 ) } = ( 𝑋 ∖ 𝑎 ) )
176 175 ineq2d ⊢ ( 𝐽 ∈ Top → ( 𝑎 ∩ ∪ { ( 𝑋 ∖ 𝑎 ) } ) = ( 𝑎 ∩ ( 𝑋 ∖ 𝑎 ) ) )
177 disjdif ⊢ ( 𝑎 ∩ ( 𝑋 ∖ 𝑎 ) ) = ∅
178 176 177 eqtrdi ⊢ ( 𝐽 ∈ Top → ( 𝑎 ∩ ∪ { ( 𝑋 ∖ 𝑎 ) } ) = ∅ )
179 inunissunidif ⊢ ( ( 𝑎 ∩ ∪ { ( 𝑋 ∖ 𝑎 ) } ) = ∅ → ( 𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
180 178 179 syl ⊢ ( 𝐽 ∈ Top → ( 𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
181 171 180 sylan9bbr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠 ) → ( 𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
182 181 biimpd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠 ) → ( 𝑎 ⊆ 𝑋 → 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
183 182 impancom ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) → ( 𝑋 = ∪ 𝑠 → 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) )
184 170 183 anim12d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) )
185 5 29 184 syl2an ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) )
186 185 adantrr ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) )
187 186 anim2d ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) ) → ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) ) )
188 120 ad2antrr ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → 𝑎 ≈ ran 𝑓 )
189 fvineqsneq ⊢ ( ( ( 𝑓 Fn 𝑎 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) = ran 𝑓 )
190 59 189 sylanl1 ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) = ran 𝑓 )
191 vex ⊢ 𝑠 ∈ V
192 difss ⊢ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑠
193 ssdomg ⊢ ( 𝑠 ∈ V → ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ 𝑠 → ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ≼ 𝑠 ) )
194 191 192 193 mp2 ⊢ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ≼ 𝑠
195 190 194 eqbrtrrdi ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → ran 𝑓 ≼ 𝑠 )
196 endomtr ⊢ ( ( 𝑎 ≈ ran 𝑓 ∧ ran 𝑓 ≼ 𝑠 ) → 𝑎 ≼ 𝑠 )
197 188 195 196 syl2anc ⊢ ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ ( 𝑠 ∖ { ( 𝑋 ∖ 𝑎 ) } ) ) ) → 𝑎 ≼ 𝑠 )
198 187 197 syl6 ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ∧ ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) ) → 𝑎 ≼ 𝑠 ) )
199 198 expdimp ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → 𝑎 ≼ 𝑠 ) )
200 elinel2 ⊢ ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) → 𝑠 ∈ Fin )
201 200 adantr ⊢ ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → 𝑠 ∈ Fin )
202 199 201 jca2 ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
203 202 eximdv ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ∃ 𝑠 ( 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑠 ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
204 161 203 biimtrid ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ( ∃ 𝑠 ∈ ( 𝒫 ( ran 𝑓 ∪ { ( 𝑋 ∖ 𝑎 ) } ) ∩ Fin ) 𝑋 = ∪ 𝑠 → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
205 160 204 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) ∧ ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) )
206 205 ex ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
207 206 exlimdv ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑎 ≈ ω ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
208 207 anass1rs ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
209 208 3adant3 ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ( ∃ 𝑓 ( 𝑓 : 𝑎 –1-1→ 𝐽 ∧ ∀ 𝑝 ∈ 𝑎 ( ( 𝑓 ‘ 𝑝 ) ∩ 𝑎 ) = { 𝑝 } ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) ) )
210 49 209 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) )
211 18 27 28 210 syl3anc ⊢ ( ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) )
212 211 anasss ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) ) → ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) )
213 isfinite ⊢ ( 𝑠 ∈ Fin ↔ 𝑠 ≺ ω )
214 domsdomtr ⊢ ( ( 𝑎 ≼ 𝑠 ∧ 𝑠 ≺ ω ) → 𝑎 ≺ ω )
215 213 214 sylan2b ⊢ ( ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) → 𝑎 ≺ ω )
216 215 exlimiv ⊢ ( ∃ 𝑠 ( 𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin ) → 𝑎 ≺ ω )
217 sdomnen ⊢ ( 𝑎 ≺ ω → ¬ 𝑎 ≈ ω )
218 212 216 217 3syl ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) ) → ¬ 𝑎 ≈ ω )
219 17 218 pm2.65da ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) → ¬ ( 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) )
220 imnan ⊢ ( ( 𝑎 ⊆ 𝑋 → ¬ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) ↔ ¬ ( 𝑎 ⊆ 𝑋 ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) )
221 219 220 sylibr ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) → ( 𝑎 ⊆ 𝑋 → ¬ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ) )
222 221 imp ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ¬ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ )
223 neq0 ⊢ ( ¬ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) = ∅ ↔ ∃ 𝑠 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) )
224 222 223 sylib ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ∃ 𝑠 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) )
225 1 lpss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑋 )
226 5 225 sylan ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑋 )
227 226 adantlr ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ 𝑋 )
228 227 sseld ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → 𝑠 ∈ 𝑋 ) )
229 228 ancrd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → ( 𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ) ) )
230 229 eximdv ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( ∃ 𝑠 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ) ) )
231 df-rex ⊢ ( ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ) )
232 230 231 imbitrrdi ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ( ∃ 𝑠 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ) )
233 224 232 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ 𝑎 ⊆ 𝑋 ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) )
234 16 233 sylan2 ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) )
235 1 lpss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
236 235 3expb ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
237 5 236 sylan ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
238 237 adantlr ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
239 238 sseld ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
240 239 reximdv ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ( ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑎 ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
241 234 240 mpd ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω ) ∧ ( 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏 ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
242 241 an42s ⊢ ( ( ( 𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋 ) ∧ ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
243 242 ex ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋 ) → ( ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
244 243 exlimdv ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋 ) → ( ∃ 𝑎 ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
245 244 adantrr ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin ) ) → ( ∃ 𝑎 ( 𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
246 14 245 mpd ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
247 8 246 sylan2b ⊢ ( ( 𝐽 ∈ 𝐶 ∧ ( 𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
248 6 247 sylan2b ⊢ ( ( 𝐽 ∈ 𝐶 ∧ 𝑏 ∈ ( 𝒫 𝑋 ∖ Fin ) ) → ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
249 248 ralrimiva ⊢ ( 𝐽 ∈ 𝐶 → ∀ 𝑏 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
250 simpr ⊢ ( ( 𝑦 = 𝑏 ∧ 𝑧 = 𝑠 ) → 𝑧 = 𝑠 )
251 fveq2 ⊢ ( 𝑦 = 𝑏 → ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
252 251 adantr ⊢ ( ( 𝑦 = 𝑏 ∧ 𝑧 = 𝑠 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
253 250 252 eleq12d ⊢ ( ( 𝑦 = 𝑏 ∧ 𝑧 = 𝑠 ) → ( 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ↔ 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
254 253 cbvrexdva ⊢ ( 𝑦 = 𝑏 → ( ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ↔ ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) ) )
255 254 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑠 ∈ 𝑋 𝑠 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑏 ) )
256 249 255 sylibr ⊢ ( 𝐽 ∈ 𝐶 → ∀ 𝑦 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) )
257 1 3 pibp21 ⊢ ( 𝐽 ∈ 𝑊 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ ( 𝒫 𝑋 ∖ Fin ) ∃ 𝑧 ∈ 𝑋 𝑧 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑦 ) ) )
258 5 256 257 sylanbrc ⊢ ( 𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊 )