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 
|- 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 infinf 
 |-  ( b e. _V -> ( -. b e. Fin <-> _om ~<_ b ) )
10 9 elv 
 |-  ( -. b e. Fin <-> _om ~<_ b )
11 vex 
 |-  b e. _V
12 11 infcntss 
 |-  ( _om ~<_ b -> E. a ( a C_ b /\ a ~~ _om ) )
13 10 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 vex 
 |-  a e. _V
31 simp1 
 |-  ( ( J e. Top /\ a C_ X /\ ( ( limPt ` J ) ` a ) = (/) ) -> J e. Top )
32 31 elexd 
 |-  ( ( J e. Top /\ a C_ X /\ ( ( limPt ` J ) ` a ) = (/) ) -> J e. _V )
33 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 } ) )
34 simpr 
 |-  ( ( p e. n /\ ( n i^i a ) = { p } ) -> ( n i^i a ) = { p } )
35 34 reximi 
 |-  ( E. n e. J ( p e. n /\ ( n i^i a ) = { p } ) -> E. n e. J ( n i^i a ) = { p } )
36 35 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 } )
37 33 36 syl 
 |-  ( ( J e. Top /\ a C_ X /\ ( ( limPt ` J ) ` a ) = (/) ) -> A. p e. a E. n e. J ( n i^i a ) = { p } )
38 ineq1 
 |-  ( n = ( f ` p ) -> ( n i^i a ) = ( ( f ` p ) i^i a ) )
39 38 eqeq1d 
 |-  ( n = ( f ` p ) -> ( ( n i^i a ) = { p } <-> ( ( f ` p ) i^i a ) = { p } ) )
40 39 ac6 
 |-  ( ( a e. _V /\ J e. _V /\ 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 } ) )
41 30 32 37 40 mp3an2i 
 |-  ( ( J e. Top /\ a C_ X /\ ( ( limPt ` J ) ` a ) = (/) ) -> E. f ( f : a --> J /\ A. p e. a ( ( f ` p ) i^i a ) = { p } ) )
42 fvineqsnf1 
 |-  ( ( f : a --> J /\ A. p e. a ( ( f ` p ) i^i a ) = { p } ) -> f : a -1-1-> J )
43 simpr 
 |-  ( ( f : a --> J /\ A. p e. a ( ( f ` p ) i^i a ) = { p } ) -> A. p e. a ( ( f ` p ) i^i a ) = { p } )
44 42 43 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 } ) )
45 44 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 } ) )
46 41 45 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 } ) )
47 29 46 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 } ) )
48 5 47 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 } ) )
49 48 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 } ) )
50 simpr 
 |-  ( ( ( J e. Top /\ a e. ( Clsd ` J ) ) /\ f : a -1-1-> J ) -> f : a -1-1-> J )
51 vsnid 
 |-  p e. { p }
52 eleq2 
 |-  ( ( ( f ` p ) i^i a ) = { p } -> ( p e. ( ( f ` p ) i^i a ) <-> p e. { p } ) )
53 51 52 mpbiri 
 |-  ( ( ( f ` p ) i^i a ) = { p } -> p e. ( ( f ` p ) i^i a ) )
54 53 elin1d 
 |-  ( ( ( f ` p ) i^i a ) = { p } -> p e. ( f ` p ) )
55 54 ralimi 
 |-  ( A. p e. a ( ( f ` p ) i^i a ) = { p } -> A. p e. a p e. ( f ` p ) )
56 ralssiun 
 |-  ( A. p e. a p e. ( f ` p ) -> a C_ U_ p e. a ( f ` p ) )
57 55 56 syl 
 |-  ( A. p e. a ( ( f ` p ) i^i a ) = { p } -> a C_ U_ p e. a ( f ` p ) )
58 57 adantl 
 |-  ( ( f : a -1-1-> J /\ A. p e. a ( ( f ` p ) i^i a ) = { p } ) -> a C_ U_ p e. a ( f ` p ) )
59 f1fn 
 |-  ( f : a -1-1-> J -> f Fn a )
60 fniunfv 
 |-  ( f Fn a -> U_ p e. a ( f ` p ) = U. ran f )
61 59 60 syl 
 |-  ( f : a -1-1-> J -> U_ p e. a ( f ` p ) = U. ran f )
62 61 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 )
63 58 62 sseqtrd 
 |-  ( ( f : a -1-1-> J /\ A. p e. a ( ( f ` p ) i^i a ) = { p } ) -> a C_ U. ran f )
64 1 cldopn 
 |-  ( a e. ( Clsd ` J ) -> ( X \ a ) e. J )
65 64 ad2antll 
 |-  ( ( f : a -1-1-> J /\ ( J e. Top /\ a e. ( Clsd ` J ) ) ) -> ( X \ a ) e. J )
66 65 anim1ci 
 |-  ( ( ( 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 ) )
67 29 ad2antll 
 |-  ( ( f : a -1-1-> J /\ ( J e. Top /\ a e. ( Clsd ` J ) ) ) -> a C_ X )
68 67 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 ) ) )
69 unisng 
 |-  ( ( X \ a ) e. J -> U. { ( X \ a ) } = ( X \ a ) )
70 69 eqcomd 
 |-  ( ( X \ a ) e. J -> ( X \ a ) = U. { ( X \ a ) } )
71 eqimss 
 |-  ( ( X \ a ) = U. { ( X \ a ) } -> ( X \ a ) C_ U. { ( X \ a ) } )
72 ssun4 
 |-  ( ( X \ a ) C_ U. { ( X \ a ) } -> ( X \ a ) C_ ( U. ran f u. U. { ( X \ a ) } ) )
73 uniun 
 |-  U. ( ran f u. { ( X \ a ) } ) = ( U. ran f u. U. { ( X \ a ) } )
74 72 73 sseqtrrdi 
 |-  ( ( X \ a ) C_ U. { ( X \ a ) } -> ( X \ a ) C_ U. ( ran f u. { ( X \ a ) } ) )
75 70 71 74 3syl 
 |-  ( ( X \ a ) e. J -> ( X \ a ) C_ U. ( ran f u. { ( X \ a ) } ) )
76 ssun3 
 |-  ( a C_ U. ran f -> a C_ ( U. ran f u. U. { ( X \ a ) } ) )
77 76 73 sseqtrrdi 
 |-  ( a C_ U. ran f -> a C_ U. ( ran f u. { ( X \ a ) } ) )
78 uncom 
 |-  ( a u. ( X \ a ) ) = ( ( X \ a ) u. a )
79 undif1 
 |-  ( ( X \ a ) u. a ) = ( X u. a )
80 78 79 eqtri 
 |-  ( a u. ( X \ a ) ) = ( X u. a )
81 ssequn2 
 |-  ( a C_ X <-> ( X u. a ) = X )
82 81 biimpi 
 |-  ( a C_ X -> ( X u. a ) = X )
83 80 82 eqtrid 
 |-  ( a C_ X -> ( a u. ( X \ a ) ) = X )
84 83 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 )
85 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 ) } ) ) )
86 unidm 
 |-  ( U. ( ran f u. { ( X \ a ) } ) u. U. ( ran f u. { ( X \ a ) } ) ) = U. ( ran f u. { ( X \ a ) } )
87 85 86 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 ) } ) )
88 87 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 ) } ) )
89 84 88 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 ) } ) )
90 77 89 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 ) } ) )
91 75 90 sylanr2 
 |-  ( ( a C_ X /\ ( a C_ U. ran f /\ ( X \ a ) e. J ) ) -> X C_ U. ( ran f u. { ( X \ a ) } ) )
92 91 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 ) } ) )
93 f1f 
 |-  ( f : a -1-1-> J -> f : a --> J )
94 93 frnd 
 |-  ( f : a -1-1-> J -> ran f C_ J )
95 1 topopn 
 |-  ( J e. Top -> X e. J )
96 1 difopn 
 |-  ( ( X e. J /\ a e. ( Clsd ` J ) ) -> ( X \ a ) e. J )
97 95 96 sylan 
 |-  ( ( J e. Top /\ a e. ( Clsd ` J ) ) -> ( X \ a ) e. J )
98 97 snssd 
 |-  ( ( J e. Top /\ a e. ( Clsd ` J ) ) -> { ( X \ a ) } C_ J )
99 unss12 
 |-  ( ( ran f C_ J /\ { ( X \ a ) } C_ J ) -> ( ran f u. { ( X \ a ) } ) C_ ( J u. J ) )
100 unidm 
 |-  ( J u. J ) = J
101 99 100 sseqtrdi 
 |-  ( ( ran f C_ J /\ { ( X \ a ) } C_ J ) -> ( ran f u. { ( X \ a ) } ) C_ J )
102 94 98 101 syl2an 
 |-  ( ( f : a -1-1-> J /\ ( J e. Top /\ a e. ( Clsd ` J ) ) ) -> ( ran f u. { ( X \ a ) } ) C_ J )
103 uniss 
 |-  ( ( ran f u. { ( X \ a ) } ) C_ J -> U. ( ran f u. { ( X \ a ) } ) C_ U. J )
104 103 1 sseqtrrdi 
 |-  ( ( ran f u. { ( X \ a ) } ) C_ J -> U. ( ran f u. { ( X \ a ) } ) C_ X )
105 102 104 syl 
 |-  ( ( f : a -1-1-> J /\ ( J e. Top /\ a e. ( Clsd ` J ) ) ) -> U. ( ran f u. { ( X \ a ) } ) C_ X )
106 105 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 )
107 92 106 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 ) } ) )
108 68 107 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 ) } ) )
109 66 108 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 ) } ) )
110 63 109 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 ) } ) )
111 110 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 ) } ) )
112 111 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 ) } ) ) )
113 50 112 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 ) } ) ) )
114 113 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 ) } ) )
115 114 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 ) } ) )
116 5 115 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 ) } ) )
117 vex 
 |-  f e. _V
118 f1f1orn 
 |-  ( f : a -1-1-> J -> f : a -1-1-onto-> ran f )
119 f1oen3g 
 |-  ( ( f e. _V /\ f : a -1-1-onto-> ran f ) -> a ~~ ran f )
120 117 118 119 sylancr 
 |-  ( f : a -1-1-> J -> a ~~ ran f )
121 enen1 
 |-  ( a ~~ ran f -> ( a ~~ _om <-> ran f ~~ _om ) )
122 endom 
 |-  ( ran f ~~ _om -> ran f ~<_ _om )
123 snfi 
 |-  { ( X \ a ) } e. Fin
124 fict 
 |-  ( { ( X \ a ) } e. Fin -> { ( 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 122 125 126 sylancl 
 |-  ( ran f ~~ _om -> ( ran f u. { ( X \ a ) } ) ~<_ _om )
128 121 127 biimtrdi 
 |-  ( a ~~ ran f -> ( a ~~ _om -> ( ran f u. { ( X \ a ) } ) ~<_ _om ) )
129 120 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 102 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 116 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 95 elexd 
 |-  ( J e. Top -> X e. _V )
173 difexg 
 |-  ( X e. _V -> ( X \ a ) e. _V )
174 unisng 
 |-  ( ( X \ a ) e. _V -> U. { ( X \ a ) } = ( X \ a ) )
175 172 173 174 3syl 
 |-  ( J e. Top -> U. { ( X \ a ) } = ( X \ a ) )
176 175 ineq2d 
 |-  ( J e. Top -> ( a i^i U. { ( X \ a ) } ) = ( a i^i ( X \ a ) ) )
177 disjdif 
 |-  ( a i^i ( X \ a ) ) = (/)
178 176 177 eqtrdi 
 |-  ( J e. Top -> ( a i^i U. { ( X \ a ) } ) = (/) )
179 inunissunidif 
 |-  ( ( a i^i U. { ( X \ a ) } ) = (/) -> ( a C_ U. s <-> a C_ U. ( s \ { ( X \ a ) } ) ) )
180 178 179 syl 
 |-  ( J e. Top -> ( a C_ U. s <-> a C_ U. ( s \ { ( X \ a ) } ) ) )
181 171 180 sylan9bbr 
 |-  ( ( J e. Top /\ X = U. s ) -> ( a C_ X <-> a C_ U. ( s \ { ( X \ a ) } ) ) )
182 181 biimpd 
 |-  ( ( J e. Top /\ X = U. s ) -> ( a C_ X -> a C_ U. ( s \ { ( X \ a ) } ) ) )
183 182 impancom 
 |-  ( ( J e. Top /\ a C_ X ) -> ( X = U. s -> a C_ U. ( s \ { ( X \ a ) } ) ) )
184 170 183 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 ) } ) ) ) )
185 5 29 184 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 ) } ) ) ) )
186 185 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 ) } ) ) ) )
187 186 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 ) } ) ) ) ) )
188 120 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 )
189 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 )
190 59 189 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 )
191 vex 
 |-  s e. _V
192 difss 
 |-  ( s \ { ( X \ a ) } ) C_ s
193 ssdomg 
 |-  ( s e. _V -> ( ( s \ { ( X \ a ) } ) C_ s -> ( s \ { ( X \ a ) } ) ~<_ s ) )
194 191 192 193 mp2 
 |-  ( s \ { ( X \ a ) } ) ~<_ s
195 190 194 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 )
196 endomtr 
 |-  ( ( a ~~ ran f /\ ran f ~<_ s ) -> a ~<_ s )
197 188 195 196 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 )
198 187 197 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 ) )
199 198 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 ) )
200 elinel2 
 |-  ( s e. ( ~P ( ran f u. { ( X \ a ) } ) i^i Fin ) -> s e. Fin )
201 200 adantr 
 |-  ( ( s e. ( ~P ( ran f u. { ( X \ a ) } ) i^i Fin ) /\ X = U. s ) -> s e. Fin )
202 199 201 jca2 
 |-  ( ( ( 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 ) ) )
203 202 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 ) ) )
204 161 203 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 ) ) )
205 160 204 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 ) )
206 205 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 ) ) )
207 206 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 ) ) )
208 207 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 ) ) )
209 208 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 ) ) )
210 49 209 mpd 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ a e. ( Clsd ` J ) /\ ( ( limPt ` J ) ` a ) = (/) ) -> E. s ( a ~<_ s /\ s e. Fin ) )
211 18 27 28 210 syl3anc 
 |-  ( ( ( ( J e. C /\ a ~~ _om ) /\ a C_ X ) /\ ( ( limPt ` J ) ` a ) = (/) ) -> E. s ( a ~<_ s /\ s e. Fin ) )
212 211 anasss 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ ( a C_ X /\ ( ( limPt ` J ) ` a ) = (/) ) ) -> E. s ( a ~<_ s /\ s e. Fin ) )
213 isfinite 
 |-  ( s e. Fin <-> s ~< _om )
214 domsdomtr 
 |-  ( ( a ~<_ s /\ s ~< _om ) -> a ~< _om )
215 213 214 sylan2b 
 |-  ( ( a ~<_ s /\ s e. Fin ) -> a ~< _om )
216 215 exlimiv 
 |-  ( E. s ( a ~<_ s /\ s e. Fin ) -> a ~< _om )
217 sdomnen 
 |-  ( a ~< _om -> -. a ~~ _om )
218 212 216 217 3syl 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ ( a C_ X /\ ( ( limPt ` J ) ` a ) = (/) ) ) -> -. a ~~ _om )
219 17 218 pm2.65da 
 |-  ( ( J e. C /\ a ~~ _om ) -> -. ( a C_ X /\ ( ( limPt ` J ) ` a ) = (/) ) )
220 imnan 
 |-  ( ( a C_ X -> -. ( ( limPt ` J ) ` a ) = (/) ) <-> -. ( a C_ X /\ ( ( limPt ` J ) ` a ) = (/) ) )
221 219 220 sylibr 
 |-  ( ( J e. C /\ a ~~ _om ) -> ( a C_ X -> -. ( ( limPt ` J ) ` a ) = (/) ) )
222 221 imp 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ a C_ X ) -> -. ( ( limPt ` J ) ` a ) = (/) )
223 neq0 
 |-  ( -. ( ( limPt ` J ) ` a ) = (/) <-> E. s s e. ( ( limPt ` J ) ` a ) )
224 222 223 sylib 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ a C_ X ) -> E. s s e. ( ( limPt ` J ) ` a ) )
225 1 lpss 
 |-  ( ( J e. Top /\ a C_ X ) -> ( ( limPt ` J ) ` a ) C_ X )
226 5 225 sylan 
 |-  ( ( J e. C /\ a C_ X ) -> ( ( limPt ` J ) ` a ) C_ X )
227 226 adantlr 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ a C_ X ) -> ( ( limPt ` J ) ` a ) C_ X )
228 227 sseld 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ a C_ X ) -> ( s e. ( ( limPt ` J ) ` a ) -> s e. X ) )
229 228 ancrd 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ a C_ X ) -> ( s e. ( ( limPt ` J ) ` a ) -> ( s e. X /\ s e. ( ( limPt ` J ) ` a ) ) ) )
230 229 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 ) ) ) )
231 df-rex 
 |-  ( E. s e. X s e. ( ( limPt ` J ) ` a ) <-> E. s ( s e. X /\ s e. ( ( limPt ` J ) ` a ) ) )
232 230 231 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 ) ) )
233 224 232 mpd 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ a C_ X ) -> E. s e. X s e. ( ( limPt ` J ) ` a ) )
234 16 233 sylan2 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ ( b C_ X /\ a C_ b ) ) -> E. s e. X s e. ( ( limPt ` J ) ` a ) )
235 1 lpss3 
 |-  ( ( J e. Top /\ b C_ X /\ a C_ b ) -> ( ( limPt ` J ) ` a ) C_ ( ( limPt ` J ) ` b ) )
236 235 3expb 
 |-  ( ( J e. Top /\ ( b C_ X /\ a C_ b ) ) -> ( ( limPt ` J ) ` a ) C_ ( ( limPt ` J ) ` b ) )
237 5 236 sylan 
 |-  ( ( J e. C /\ ( b C_ X /\ a C_ b ) ) -> ( ( limPt ` J ) ` a ) C_ ( ( limPt ` J ) ` b ) )
238 237 adantlr 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ ( b C_ X /\ a C_ b ) ) -> ( ( limPt ` J ) ` a ) C_ ( ( limPt ` J ) ` b ) )
239 238 sseld 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ ( b C_ X /\ a C_ b ) ) -> ( s e. ( ( limPt ` J ) ` a ) -> s e. ( ( limPt ` J ) ` b ) ) )
240 239 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 ) ) )
241 234 240 mpd 
 |-  ( ( ( J e. C /\ a ~~ _om ) /\ ( b C_ X /\ a C_ b ) ) -> E. s e. X s e. ( ( limPt ` J ) ` b ) )
242 241 an42s 
 |-  ( ( ( J e. C /\ b C_ X ) /\ ( a C_ b /\ a ~~ _om ) ) -> E. s e. X s e. ( ( limPt ` J ) ` b ) )
243 242 ex 
 |-  ( ( J e. C /\ b C_ X ) -> ( ( a C_ b /\ a ~~ _om ) -> E. s e. X s e. ( ( limPt ` J ) ` b ) ) )
244 243 exlimdv 
 |-  ( ( J e. C /\ b C_ X ) -> ( E. a ( a C_ b /\ a ~~ _om ) -> E. s e. X s e. ( ( limPt ` J ) ` b ) ) )
245 244 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 ) ) )
246 14 245 mpd 
 |-  ( ( J e. C /\ ( b C_ X /\ -. b e. Fin ) ) -> E. s e. X s e. ( ( limPt ` J ) ` b ) )
247 8 246 sylan2b 
 |-  ( ( J e. C /\ ( b e. ~P X /\ -. b e. Fin ) ) -> E. s e. X s e. ( ( limPt ` J ) ` b ) )
248 6 247 sylan2b 
 |-  ( ( J e. C /\ b e. ( ~P X \ Fin ) ) -> E. s e. X s e. ( ( limPt ` J ) ` b ) )
249 248 ralrimiva 
 |-  ( J e. C -> A. b e. ( ~P X \ Fin ) E. s e. X s e. ( ( limPt ` J ) ` b ) )
250 simpr 
 |-  ( ( y = b /\ z = s ) -> z = s )
251 fveq2 
 |-  ( y = b -> ( ( limPt ` J ) ` y ) = ( ( limPt ` J ) ` b ) )
252 251 adantr 
 |-  ( ( y = b /\ z = s ) -> ( ( limPt ` J ) ` y ) = ( ( limPt ` J ) ` b ) )
253 250 252 eleq12d 
 |-  ( ( y = b /\ z = s ) -> ( z e. ( ( limPt ` J ) ` y ) <-> s e. ( ( limPt ` J ) ` b ) ) )
254 253 cbvrexdva 
 |-  ( y = b -> ( E. z e. X z e. ( ( limPt ` J ) ` y ) <-> E. s e. X s e. ( ( limPt ` J ) ` b ) ) )
255 254 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 ) )
256 249 255 sylibr 
 |-  ( J e. C -> A. y e. ( ~P X \ Fin ) E. z e. X z e. ( ( limPt ` J ) ` y ) )
257 1 3 pibp21 
 |-  ( J e. W <-> ( J e. Top /\ A. y e. ( ~P X \ Fin ) E. z e. X z e. ( ( limPt ` J ) ` y ) ) )
258 5 256 257 sylanbrc 
 |-  ( J e. C -> J e. W )