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 
|- X = U. J
pibt2.19 
|- C = { x e. Top | A. y e. ~P x ( ( U. x = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }
pibt2.21 
|- W = { x e. Top | A. y e. ( ~P U. x \ Fin ) E. z e. U. x z e. ( ( limPt ` x ) ` y ) }
Assertion pibt2 
|- ( J e. C -> J e. W )

Proof

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