Metamath Proof Explorer

Theorem cmpcld

Description: A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009)

Ref Expression
Assertion cmpcld 
|- ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> ( J |`t S ) e. Comp )

Proof

Step Hyp Ref Expression
1 velpw 
 |-  ( s e. ~P J <-> s C_ J )
2 simp1l 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> J e. Comp )
3 simp2 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> s C_ J )
4 eqid 
 |-  U. J = U. J
5 4 cldopn 
 |-  ( S e. ( Clsd ` J ) -> ( U. J \ S ) e. J )
6 5 adantl 
 |-  ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> ( U. J \ S ) e. J )
7 6 3ad2ant1 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( U. J \ S ) e. J )
8 7 snssd 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> { ( U. J \ S ) } C_ J )
9 3 8 unssd 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( s u. { ( U. J \ S ) } ) C_ J )
10 simp3 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> S C_ U. s )
11 uniss 
 |-  ( s C_ J -> U. s C_ U. J )
12 11 3ad2ant2 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. s C_ U. J )
13 10 12 sstrd 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> S C_ U. J )
14 undif 
 |-  ( S C_ U. J <-> ( S u. ( U. J \ S ) ) = U. J )
15 13 14 sylib 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( S u. ( U. J \ S ) ) = U. J )
16 unss1 
 |-  ( S C_ U. s -> ( S u. ( U. J \ S ) ) C_ ( U. s u. ( U. J \ S ) ) )
17 16 3ad2ant3 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( S u. ( U. J \ S ) ) C_ ( U. s u. ( U. J \ S ) ) )
18 15 17 eqsstrrd 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. J C_ ( U. s u. ( U. J \ S ) ) )
19 difss 
 |-  ( U. J \ S ) C_ U. J
20 unss 
 |-  ( ( U. s C_ U. J /\ ( U. J \ S ) C_ U. J ) <-> ( U. s u. ( U. J \ S ) ) C_ U. J )
21 12 19 20 sylanblc 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( U. s u. ( U. J \ S ) ) C_ U. J )
22 18 21 eqssd 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. J = ( U. s u. ( U. J \ S ) ) )
23 uniexg 
 |-  ( J e. Comp -> U. J e. _V )
24 23 ad2antrr 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J ) -> U. J e. _V )
25 24 3adant3 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. J e. _V )
26 difexg 
 |-  ( U. J e. _V -> ( U. J \ S ) e. _V )
27 unisng 
 |-  ( ( U. J \ S ) e. _V -> U. { ( U. J \ S ) } = ( U. J \ S ) )
28 25 26 27 3syl 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. { ( U. J \ S ) } = ( U. J \ S ) )
29 28 uneq2d 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( U. s u. U. { ( U. J \ S ) } ) = ( U. s u. ( U. J \ S ) ) )
30 22 29 eqtr4d 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. J = ( U. s u. U. { ( U. J \ S ) } ) )
31 uniun 
 |-  U. ( s u. { ( U. J \ S ) } ) = ( U. s u. U. { ( U. J \ S ) } )
32 30 31 eqtr4di 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. J = U. ( s u. { ( U. J \ S ) } ) )
33 4 cmpcov 
 |-  ( ( J e. Comp /\ ( s u. { ( U. J \ S ) } ) C_ J /\ U. J = U. ( s u. { ( U. J \ S ) } ) ) -> E. u e. ( ~P ( s u. { ( U. J \ S ) } ) i^i Fin ) U. J = U. u )
34 2 9 32 33 syl3anc 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> E. u e. ( ~P ( s u. { ( U. J \ S ) } ) i^i Fin ) U. J = U. u )
35 elfpw 
 |-  ( u e. ( ~P ( s u. { ( U. J \ S ) } ) i^i Fin ) <-> ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) )
36 simp2l 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> u C_ ( s u. { ( U. J \ S ) } ) )
37 uncom 
 |-  ( s u. { ( U. J \ S ) } ) = ( { ( U. J \ S ) } u. s )
38 36 37 sseqtrdi 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> u C_ ( { ( U. J \ S ) } u. s ) )
39 ssundif 
 |-  ( u C_ ( { ( U. J \ S ) } u. s ) <-> ( u \ { ( U. J \ S ) } ) C_ s )
40 38 39 sylib 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> ( u \ { ( U. J \ S ) } ) C_ s )
41 diffi 
 |-  ( u e. Fin -> ( u \ { ( U. J \ S ) } ) e. Fin )
42 41 ad2antll 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) ) -> ( u \ { ( U. J \ S ) } ) e. Fin )
43 42 3adant3 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> ( u \ { ( U. J \ S ) } ) e. Fin )
44 elfpw 
 |-  ( ( u \ { ( U. J \ S ) } ) e. ( ~P s i^i Fin ) <-> ( ( u \ { ( U. J \ S ) } ) C_ s /\ ( u \ { ( U. J \ S ) } ) e. Fin ) )
45 40 43 44 sylanbrc 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> ( u \ { ( U. J \ S ) } ) e. ( ~P s i^i Fin ) )
46 10 3ad2ant1 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> S C_ U. s )
47 12 3ad2ant1 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> U. s C_ U. J )
48 simp3 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> U. J = U. u )
49 47 48 sseqtrd 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> U. s C_ U. u )
50 46 49 sstrd 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> S C_ U. u )
51 50 sselda 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> v e. U. u )
52 eluni 
 |-  ( v e. U. u <-> E. w ( v e. w /\ w e. u ) )
53 51 52 sylib 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> E. w ( v e. w /\ w e. u ) )
54 simpl 
 |-  ( ( v e. w /\ w e. u ) -> v e. w )
55 54 a1i 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( ( v e. w /\ w e. u ) -> v e. w ) )
56 simpr 
 |-  ( ( v e. w /\ w e. u ) -> w e. u )
57 56 a1i 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( ( v e. w /\ w e. u ) -> w e. u ) )
58 elndif 
 |-  ( v e. S -> -. v e. ( U. J \ S ) )
59 58 ad2antlr 
 |-  ( ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) /\ v e. w ) -> -. v e. ( U. J \ S ) )
60 eleq2 
 |-  ( w = ( U. J \ S ) -> ( v e. w <-> v e. ( U. J \ S ) ) )
61 60 biimpd 
 |-  ( w = ( U. J \ S ) -> ( v e. w -> v e. ( U. J \ S ) ) )
62 61 a1i 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( w = ( U. J \ S ) -> ( v e. w -> v e. ( U. J \ S ) ) ) )
63 62 com23 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( v e. w -> ( w = ( U. J \ S ) -> v e. ( U. J \ S ) ) ) )
64 63 imp 
 |-  ( ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) /\ v e. w ) -> ( w = ( U. J \ S ) -> v e. ( U. J \ S ) ) )
65 59 64 mtod 
 |-  ( ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) /\ v e. w ) -> -. w = ( U. J \ S ) )
66 65 ex 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( v e. w -> -. w = ( U. J \ S ) ) )
67 66 adantrd 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( ( v e. w /\ w e. u ) -> -. w = ( U. J \ S ) ) )
68 velsn 
 |-  ( w e. { ( U. J \ S ) } <-> w = ( U. J \ S ) )
69 68 notbii 
 |-  ( -. w e. { ( U. J \ S ) } <-> -. w = ( U. J \ S ) )
70 67 69 syl6ibr 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( ( v e. w /\ w e. u ) -> -. w e. { ( U. J \ S ) } ) )
71 57 70 jcad 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( ( v e. w /\ w e. u ) -> ( w e. u /\ -. w e. { ( U. J \ S ) } ) ) )
72 eldif 
 |-  ( w e. ( u \ { ( U. J \ S ) } ) <-> ( w e. u /\ -. w e. { ( U. J \ S ) } ) )
73 71 72 syl6ibr 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( ( v e. w /\ w e. u ) -> w e. ( u \ { ( U. J \ S ) } ) ) )
74 55 73 jcad 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( ( v e. w /\ w e. u ) -> ( v e. w /\ w e. ( u \ { ( U. J \ S ) } ) ) ) )
75 74 eximdv 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> ( E. w ( v e. w /\ w e. u ) -> E. w ( v e. w /\ w e. ( u \ { ( U. J \ S ) } ) ) ) )
76 53 75 mpd 
 |-  ( ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) /\ v e. S ) -> E. w ( v e. w /\ w e. ( u \ { ( U. J \ S ) } ) ) )
77 76 ex 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> ( v e. S -> E. w ( v e. w /\ w e. ( u \ { ( U. J \ S ) } ) ) ) )
78 eluni 
 |-  ( v e. U. ( u \ { ( U. J \ S ) } ) <-> E. w ( v e. w /\ w e. ( u \ { ( U. J \ S ) } ) ) )
79 77 78 syl6ibr 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> ( v e. S -> v e. U. ( u \ { ( U. J \ S ) } ) ) )
80 79 ssrdv 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> S C_ U. ( u \ { ( U. J \ S ) } ) )
81 unieq 
 |-  ( t = ( u \ { ( U. J \ S ) } ) -> U. t = U. ( u \ { ( U. J \ S ) } ) )
82 81 sseq2d 
 |-  ( t = ( u \ { ( U. J \ S ) } ) -> ( S C_ U. t <-> S C_ U. ( u \ { ( U. J \ S ) } ) ) )
83 82 rspcev 
 |-  ( ( ( u \ { ( U. J \ S ) } ) e. ( ~P s i^i Fin ) /\ S C_ U. ( u \ { ( U. J \ S ) } ) ) -> E. t e. ( ~P s i^i Fin ) S C_ U. t )
84 45 80 83 syl2anc 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) /\ U. J = U. u ) -> E. t e. ( ~P s i^i Fin ) S C_ U. t )
85 35 84 syl3an2b 
 |-  ( ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) /\ u e. ( ~P ( s u. { ( U. J \ S ) } ) i^i Fin ) /\ U. J = U. u ) -> E. t e. ( ~P s i^i Fin ) S C_ U. t )
86 85 rexlimdv3a 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( E. u e. ( ~P ( s u. { ( U. J \ S ) } ) i^i Fin ) U. J = U. u -> E. t e. ( ~P s i^i Fin ) S C_ U. t ) )
87 34 86 mpd 
 |-  ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> E. t e. ( ~P s i^i Fin ) S C_ U. t )
88 87 3exp 
 |-  ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> ( s C_ J -> ( S C_ U. s -> E. t e. ( ~P s i^i Fin ) S C_ U. t ) ) )
89 1 88 syl5bi 
 |-  ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> ( s e. ~P J -> ( S C_ U. s -> E. t e. ( ~P s i^i Fin ) S C_ U. t ) ) )
90 89 ralrimiv 
 |-  ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> A. s e. ~P J ( S C_ U. s -> E. t e. ( ~P s i^i Fin ) S C_ U. t ) )
91 cmptop 
 |-  ( J e. Comp -> J e. Top )
92 4 cldss 
 |-  ( S e. ( Clsd ` J ) -> S C_ U. J )
93 4 cmpsub 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( J |`t S ) e. Comp <-> A. s e. ~P J ( S C_ U. s -> E. t e. ( ~P s i^i Fin ) S C_ U. t ) ) )
94 91 92 93 syl2an 
 |-  ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> ( ( J |`t S ) e. Comp <-> A. s e. ~P J ( S C_ U. s -> E. t e. ( ~P s i^i Fin ) S C_ U. t ) ) )
95 90 94 mpbird 
 |-  ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> ( J |`t S ) e. Comp )