Metamath Proof Explorer

Theorem cmpsub

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman'sBeginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis cmpsub.1 
|- X = U. J
Assertion cmpsub 
|- ( ( J e. Top /\ S C_ X ) -> ( ( J |`t S ) e. Comp <-> A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )

Proof

Step Hyp Ref Expression
1 cmpsub.1 
 |-  X = U. J
2 eqid 
 |-  U. ( J |`t S ) = U. ( J |`t S )
3 2 iscmp 
 |-  ( ( J |`t S ) e. Comp <-> ( ( J |`t S ) e. Top /\ A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) )
4 id 
 |-  ( S C_ X -> S C_ X )
5 1 topopn 
 |-  ( J e. Top -> X e. J )
6 ssexg 
 |-  ( ( S C_ X /\ X e. J ) -> S e. _V )
7 4 5 6 syl2anr 
 |-  ( ( J e. Top /\ S C_ X ) -> S e. _V )
8 resttop 
 |-  ( ( J e. Top /\ S e. _V ) -> ( J |`t S ) e. Top )
9 7 8 syldan 
 |-  ( ( J e. Top /\ S C_ X ) -> ( J |`t S ) e. Top )
10 ibar 
 |-  ( ( J |`t S ) e. Top -> ( A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) <-> ( ( J |`t S ) e. Top /\ A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) ) )
11 10 bicomd 
 |-  ( ( J |`t S ) e. Top -> ( ( ( J |`t S ) e. Top /\ A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) <-> A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) )
12 9 11 syl 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( ( J |`t S ) e. Top /\ A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) <-> A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) )
13 3 12 syl5bb 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( J |`t S ) e. Comp <-> A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) )
14 vex 
 |-  t e. _V
15 eqeq1 
 |-  ( x = t -> ( x = ( y i^i S ) <-> t = ( y i^i S ) ) )
16 15 rexbidv 
 |-  ( x = t -> ( E. y e. c x = ( y i^i S ) <-> E. y e. c t = ( y i^i S ) ) )
17 14 16 elab 
 |-  ( t e. { x | E. y e. c x = ( y i^i S ) } <-> E. y e. c t = ( y i^i S ) )
18 velpw 
 |-  ( c e. ~P J <-> c C_ J )
19 ssel2 
 |-  ( ( c C_ J /\ y e. c ) -> y e. J )
20 ineq1 
 |-  ( d = y -> ( d i^i S ) = ( y i^i S ) )
21 20 rspceeqv 
 |-  ( ( y e. J /\ t = ( y i^i S ) ) -> E. d e. J t = ( d i^i S ) )
22 21 ex 
 |-  ( y e. J -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
23 19 22 syl 
 |-  ( ( c C_ J /\ y e. c ) -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
24 23 ex 
 |-  ( c C_ J -> ( y e. c -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) ) )
25 18 24 sylbi 
 |-  ( c e. ~P J -> ( y e. c -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) ) )
26 25 adantl 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( y e. c -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) ) )
27 26 rexlimdv 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( E. y e. c t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
28 simpll 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> J e. Top )
29 1 sseq2i 
 |-  ( S C_ X <-> S C_ U. J )
30 uniexg 
 |-  ( J e. Top -> U. J e. _V )
31 ssexg 
 |-  ( ( S C_ U. J /\ U. J e. _V ) -> S e. _V )
32 30 31 sylan2 
 |-  ( ( S C_ U. J /\ J e. Top ) -> S e. _V )
33 32 ancoms 
 |-  ( ( J e. Top /\ S C_ U. J ) -> S e. _V )
34 29 33 sylan2b 
 |-  ( ( J e. Top /\ S C_ X ) -> S e. _V )
35 34 adantr 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> S e. _V )
36 elrest 
 |-  ( ( J e. Top /\ S e. _V ) -> ( t e. ( J |`t S ) <-> E. d e. J t = ( d i^i S ) ) )
37 28 35 36 syl2anc 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( t e. ( J |`t S ) <-> E. d e. J t = ( d i^i S ) ) )
38 27 37 sylibrd 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( E. y e. c t = ( y i^i S ) -> t e. ( J |`t S ) ) )
39 17 38 syl5bi 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( t e. { x | E. y e. c x = ( y i^i S ) } -> t e. ( J |`t S ) ) )
40 39 ssrdv 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> { x | E. y e. c x = ( y i^i S ) } C_ ( J |`t S ) )
41 vex 
 |-  c e. _V
42 41 abrexex 
 |-  { x | E. y e. c x = ( y i^i S ) } e. _V
43 42 elpw 
 |-  ( { x | E. y e. c x = ( y i^i S ) } e. ~P ( J |`t S ) <-> { x | E. y e. c x = ( y i^i S ) } C_ ( J |`t S ) )
44 40 43 sylibr 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> { x | E. y e. c x = ( y i^i S ) } e. ~P ( J |`t S ) )
45 unieq 
 |-  ( s = { x | E. y e. c x = ( y i^i S ) } -> U. s = U. { x | E. y e. c x = ( y i^i S ) } )
46 45 eqeq2d 
 |-  ( s = { x | E. y e. c x = ( y i^i S ) } -> ( U. ( J |`t S ) = U. s <-> U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } ) )
47 pweq 
 |-  ( s = { x | E. y e. c x = ( y i^i S ) } -> ~P s = ~P { x | E. y e. c x = ( y i^i S ) } )
48 47 ineq1d 
 |-  ( s = { x | E. y e. c x = ( y i^i S ) } -> ( ~P s i^i Fin ) = ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) )
49 48 rexeqdv 
 |-  ( s = { x | E. y e. c x = ( y i^i S ) } -> ( E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t <-> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) )
50 46 49 imbi12d 
 |-  ( s = { x | E. y e. c x = ( y i^i S ) } -> ( ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) <-> ( U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) ) )
51 50 rspcva 
 |-  ( ( { x | E. y e. c x = ( y i^i S ) } e. ~P ( J |`t S ) /\ A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) -> ( U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) )
52 44 51 sylan 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) -> ( U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) )
53 52 ex 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) -> ( U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) ) )
54 1 restuni 
 |-  ( ( J e. Top /\ S C_ X ) -> S = U. ( J |`t S ) )
55 54 ad2antrr 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> S = U. ( J |`t S ) )
56 vex 
 |-  y e. _V
57 56 inex1 
 |-  ( y i^i S ) e. _V
58 57 dfiun2 
 |-  U_ y e. c ( y i^i S ) = U. { x | E. y e. c x = ( y i^i S ) }
59 incom 
 |-  ( y i^i S ) = ( S i^i y )
60 59 a1i 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ y e. c ) -> ( y i^i S ) = ( S i^i y ) )
61 60 iuneq2dv 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> U_ y e. c ( y i^i S ) = U_ y e. c ( S i^i y ) )
62 58 61 eqtr3id 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> U. { x | E. y e. c x = ( y i^i S ) } = U_ y e. c ( S i^i y ) )
63 iunin2 
 |-  U_ y e. c ( S i^i y ) = ( S i^i U_ y e. c y )
64 uniiun 
 |-  U. c = U_ y e. c y
65 64 eqcomi 
 |-  U_ y e. c y = U. c
66 65 a1i 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> U_ y e. c y = U. c )
67 66 ineq2d 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S i^i U_ y e. c y ) = ( S i^i U. c ) )
68 incom 
 |-  ( S i^i U. c ) = ( U. c i^i S )
69 sseqin2 
 |-  ( S C_ U. c <-> ( U. c i^i S ) = S )
70 69 biimpi 
 |-  ( S C_ U. c -> ( U. c i^i S ) = S )
71 68 70 syl5eq 
 |-  ( S C_ U. c -> ( S i^i U. c ) = S )
72 71 adantl 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S i^i U. c ) = S )
73 67 72 eqtrd 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S i^i U_ y e. c y ) = S )
74 63 73 syl5eq 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> U_ y e. c ( S i^i y ) = S )
75 62 74 eqtr2d 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> S = U. { x | E. y e. c x = ( y i^i S ) } )
76 55 75 eqeq12d 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S = S <-> U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } ) )
77 55 eqeq1d 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S = U. t <-> U. ( J |`t S ) = U. t ) )
78 77 rexbidv 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t <-> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) )
79 76 78 imbi12d 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( ( S = S -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t ) <-> ( U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) ) )
80 eqid 
 |-  S = S
81 80 a1bi 
 |-  ( E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t <-> ( S = S -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t ) )
82 elin 
 |-  ( t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) <-> ( t e. ~P { x | E. y e. c x = ( y i^i S ) } /\ t e. Fin ) )
83 velpw 
 |-  ( t e. ~P { x | E. y e. c x = ( y i^i S ) } <-> t C_ { x | E. y e. c x = ( y i^i S ) } )
84 dfss3 
 |-  ( t C_ { x | E. y e. c x = ( y i^i S ) } <-> A. s e. t s e. { x | E. y e. c x = ( y i^i S ) } )
85 vex 
 |-  s e. _V
86 eqeq1 
 |-  ( x = s -> ( x = ( y i^i S ) <-> s = ( y i^i S ) ) )
87 86 rexbidv 
 |-  ( x = s -> ( E. y e. c x = ( y i^i S ) <-> E. y e. c s = ( y i^i S ) ) )
88 85 87 elab 
 |-  ( s e. { x | E. y e. c x = ( y i^i S ) } <-> E. y e. c s = ( y i^i S ) )
89 88 ralbii 
 |-  ( A. s e. t s e. { x | E. y e. c x = ( y i^i S ) } <-> A. s e. t E. y e. c s = ( y i^i S ) )
90 83 84 89 3bitri 
 |-  ( t e. ~P { x | E. y e. c x = ( y i^i S ) } <-> A. s e. t E. y e. c s = ( y i^i S ) )
91 90 anbi1i 
 |-  ( ( t e. ~P { x | E. y e. c x = ( y i^i S ) } /\ t e. Fin ) <-> ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) )
92 82 91 bitri 
 |-  ( t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) <-> ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) )
93 ineq1 
 |-  ( y = ( f ` s ) -> ( y i^i S ) = ( ( f ` s ) i^i S ) )
94 93 eqeq2d 
 |-  ( y = ( f ` s ) -> ( s = ( y i^i S ) <-> s = ( ( f ` s ) i^i S ) ) )
95 94 ac6sfi 
 |-  ( ( t e. Fin /\ A. s e. t E. y e. c s = ( y i^i S ) ) -> E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) )
96 95 ancoms 
 |-  ( ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) -> E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) )
97 96 adantl 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) )
98 frn 
 |-  ( f : t --> c -> ran f C_ c )
99 98 ad2antrl 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f C_ c )
100 vex 
 |-  f e. _V
101 100 rnex 
 |-  ran f e. _V
102 101 elpw 
 |-  ( ran f e. ~P c <-> ran f C_ c )
103 99 102 sylibr 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f e. ~P c )
104 simprr 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> t e. Fin )
105 104 ad2antrr 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> t e. Fin )
106 ffn 
 |-  ( f : t --> c -> f Fn t )
107 dffn4 
 |-  ( f Fn t <-> f : t -onto-> ran f )
108 106 107 sylib 
 |-  ( f : t --> c -> f : t -onto-> ran f )
109 fodomfi 
 |-  ( ( t e. Fin /\ f : t -onto-> ran f ) -> ran f ~<_ t )
110 108 109 sylan2 
 |-  ( ( t e. Fin /\ f : t --> c ) -> ran f ~<_ t )
111 110 adantll 
 |-  ( ( ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) /\ f : t --> c ) -> ran f ~<_ t )
112 111 adantll 
 |-  ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ f : t --> c ) -> ran f ~<_ t )
113 112 ad2ant2r 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f ~<_ t )
114 domfi 
 |-  ( ( t e. Fin /\ ran f ~<_ t ) -> ran f e. Fin )
115 105 113 114 syl2anc 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f e. Fin )
116 103 115 elind 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f e. ( ~P c i^i Fin ) )
117 id 
 |-  ( s = u -> s = u )
118 fveq2 
 |-  ( s = u -> ( f ` s ) = ( f ` u ) )
119 118 ineq1d 
 |-  ( s = u -> ( ( f ` s ) i^i S ) = ( ( f ` u ) i^i S ) )
120 117 119 eqeq12d 
 |-  ( s = u -> ( s = ( ( f ` s ) i^i S ) <-> u = ( ( f ` u ) i^i S ) ) )
121 120 rspccv 
 |-  ( A. s e. t s = ( ( f ` s ) i^i S ) -> ( u e. t -> u = ( ( f ` u ) i^i S ) ) )
122 pm2.27 
 |-  ( u e. t -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> u = ( ( f ` u ) i^i S ) ) )
123 inss1 
 |-  ( ( f ` u ) i^i S ) C_ ( f ` u )
124 sseq1 
 |-  ( u = ( ( f ` u ) i^i S ) -> ( u C_ ( f ` u ) <-> ( ( f ` u ) i^i S ) C_ ( f ` u ) ) )
125 123 124 mpbiri 
 |-  ( u = ( ( f ` u ) i^i S ) -> u C_ ( f ` u ) )
126 ssel 
 |-  ( u C_ ( f ` u ) -> ( w e. u -> w e. ( f ` u ) ) )
127 126 a1dd 
 |-  ( u C_ ( f ` u ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) )
128 125 127 syl 
 |-  ( u = ( ( f ` u ) i^i S ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) )
129 128 a1i 
 |-  ( u e. t -> ( u = ( ( f ` u ) i^i S ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) ) )
130 129 3imp 
 |-  ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> w e. ( f ` u ) ) )
131 fnfvelrn 
 |-  ( ( f Fn t /\ u e. t ) -> ( f ` u ) e. ran f )
132 131 expcom 
 |-  ( u e. t -> ( f Fn t -> ( f ` u ) e. ran f ) )
133 132 3ad2ant1 
 |-  ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f Fn t -> ( f ` u ) e. ran f ) )
134 106 133 syl5 
 |-  ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> ( f ` u ) e. ran f ) )
135 130 134 jcad 
 |-  ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
136 135 3exp 
 |-  ( u e. t -> ( u = ( ( f ` u ) i^i S ) -> ( w e. u -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) ) )
137 122 136 syld 
 |-  ( u e. t -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> ( w e. u -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) ) )
138 137 com3r 
 |-  ( w e. u -> ( u e. t -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) ) )
139 138 imp 
 |-  ( ( w e. u /\ u e. t ) -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) )
140 139 com3l 
 |-  ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> ( f : t --> c -> ( ( w e. u /\ u e. t ) -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) )
141 140 impcom 
 |-  ( ( f : t --> c /\ ( u e. t -> u = ( ( f ` u ) i^i S ) ) ) -> ( ( w e. u /\ u e. t ) -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
142 121 141 sylan2 
 |-  ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( ( w e. u /\ u e. t ) -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
143 fvex 
 |-  ( f ` u ) e. _V
144 eleq2 
 |-  ( v = ( f ` u ) -> ( w e. v <-> w e. ( f ` u ) ) )
145 eleq1 
 |-  ( v = ( f ` u ) -> ( v e. ran f <-> ( f ` u ) e. ran f ) )
146 144 145 anbi12d 
 |-  ( v = ( f ` u ) -> ( ( w e. v /\ v e. ran f ) <-> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
147 143 146 spcev 
 |-  ( ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) -> E. v ( w e. v /\ v e. ran f ) )
148 142 147 syl6 
 |-  ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( ( w e. u /\ u e. t ) -> E. v ( w e. v /\ v e. ran f ) ) )
149 148 exlimdv 
 |-  ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( E. u ( w e. u /\ u e. t ) -> E. v ( w e. v /\ v e. ran f ) ) )
150 eluni 
 |-  ( w e. U. t <-> E. u ( w e. u /\ u e. t ) )
151 eluni 
 |-  ( w e. U. ran f <-> E. v ( w e. v /\ v e. ran f ) )
152 149 150 151 3imtr4g 
 |-  ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( w e. U. t -> w e. U. ran f ) )
153 152 ssrdv 
 |-  ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> U. t C_ U. ran f )
154 153 adantl 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> U. t C_ U. ran f )
155 sseq1 
 |-  ( S = U. t -> ( S C_ U. ran f <-> U. t C_ U. ran f ) )
156 155 ad2antlr 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ( S C_ U. ran f <-> U. t C_ U. ran f ) )
157 154 156 mpbird 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> S C_ U. ran f )
158 116 157 jca 
 |-  ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) )
159 158 ex 
 |-  ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) -> ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) ) )
160 159 eximdv 
 |-  ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) -> ( E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> E. f ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) ) )
161 160 ex 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> ( S = U. t -> ( E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> E. f ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) ) ) )
162 161 com23 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> ( E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( S = U. t -> E. f ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) ) ) )
163 unieq 
 |-  ( d = ran f -> U. d = U. ran f )
164 163 sseq2d 
 |-  ( d = ran f -> ( S C_ U. d <-> S C_ U. ran f ) )
165 164 rspcev 
 |-  ( ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d )
166 165 exlimiv 
 |-  ( E. f ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d )
167 162 166 syl8 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> ( E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( S = U. t -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
168 97 167 mpd 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> ( S = U. t -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
169 92 168 sylan2b 
 |-  ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) ) -> ( S = U. t -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
170 169 rexlimdva 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
171 81 170 syl5bir 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( ( S = S -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
172 79 171 sylbird 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( ( U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
173 172 ex 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( S C_ U. c -> ( ( U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
174 173 com23 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( ( U. ( J |`t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J |`t S ) = U. t ) -> ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
175 53 174 syld 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) -> ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
176 175 ralrimdva 
 |-  ( ( J e. Top /\ S C_ X ) -> ( A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) -> A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
177 1 cmpsublem 
 |-  ( ( J e. Top /\ S C_ X ) -> ( A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) -> A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) ) )
178 176 177 impbid 
 |-  ( ( J e. Top /\ S C_ X ) -> ( A. s e. ~P ( J |`t S ) ( U. ( J |`t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J |`t S ) = U. t ) <-> A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
179 13 178 bitrd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( J |`t S ) e. Comp <-> A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )