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