MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cmpcld Structured version   Visualization version   Unicode version
Theorem cmpcld 21205
Description: A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.)
Assertion
Ref Expression
cmpcld |- ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> ( J ↾t S ) e. Comp )
Proof of Theorem cmpcld
Dummy variables t s u v w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 selpw 4165 . . . 4 |- ( s e. ~P J <-> s C_ J )
2 simp1l 1085 . . . . . . 7 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> J e. Comp )
3 simp2 1062 . . . . . . . 8 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> s C_ J )
4 eqid 2622 . . . . . . . . . . . 12 |- U. J = U. J
54cldopn 20835 . . . . . . . . . . 11 |- ( S e. ( Clsd ` J ) -> ( U. J \ S ) e. J )
65adantl 482 . . . . . . . . . 10 |- ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> ( U. J \ S ) e. J )
763ad2ant1 1082 . . . . . . . . 9 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( U. J \ S ) e. J )
87snssd 4340 . . . . . . . 8 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> { ( U. J \ S ) } C_ J )
93, 8unssd 3789 . . . . . . 7 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( s u. { ( U. J \ S ) } ) C_ J )
10 simp3 1063 . . . . . . . . . . . . 13 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> S C_ U. s )
11 uniss 4458 . . . . . . . . . . . . . 14 |- ( s C_ J -> U. s C_ U. J )
12113ad2ant2 1083 . . . . . . . . . . . . 13 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. s C_ U. J )
1310, 12sstrd 3613 . . . . . . . . . . . 12 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> S C_ U. J )
14 undif 4049 . . . . . . . . . . . 12 |- ( S C_ U. J <-> ( S u. ( U. J \ S ) ) = U. J )
1513, 14sylib 208 . . . . . . . . . . 11 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( S u. ( U. J \ S ) ) = U. J )
16 unss1 3782 . . . . . . . . . . . 12 |- ( S C_ U. s -> ( S u. ( U. J \ S ) ) C_ ( U. s u. ( U. J \ S ) ) )
17163ad2ant3 1084 . . . . . . . . . . 11 |- ( ( ( 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 ) ) )
1815, 17eqsstr3d 3640 . . . . . . . . . 10 |- ( ( ( 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 3737 . . . . . . . . . . 11 |- ( U. J \ S ) C_ U. J
20 unss 3787 . . . . . . . . . . 11 |- ( ( U. s C_ U. J /\ ( U. J \ S ) C_ U. J ) <-> ( U. s u. ( U. J \ S ) ) C_ U. J )
2112, 19, 20sylanblc 696 . . . . . . . . . 10 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> ( U. s u. ( U. J \ S ) ) C_ U. J )
2218, 21eqssd 3620 . . . . . . . . 9 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. J = ( U. s u. ( U. J \ S ) ) )
23 uniexg 6955 . . . . . . . . . . . . 13 |- ( J e. Comp -> U. J e. _V )
2423ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J ) -> U. J e. _V )
25243adant3 1081 . . . . . . . . . . 11 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. J e. _V )
26 difexg 4808 . . . . . . . . . . 11 |- ( U. J e. _V -> ( U. J \ S ) e. _V )
27 unisng 4452 . . . . . . . . . . 11 |- ( ( U. J \ S ) e. _V -> U. { ( U. J \ S ) } = ( U. J \ S ) )
2825, 26, 273syl 18 . . . . . . . . . 10 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. { ( U. J \ S ) } = ( U. J \ S ) )
2928uneq2d 3767 . . . . . . . . 9 |- ( ( ( 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 ) ) )
3022, 29eqtr4d 2659 . . . . . . . 8 |- ( ( ( 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 4456 . . . . . . . 8 |- U. ( s u. { ( U. J \ S ) } ) = ( U. s u. U. { ( U. J \ S ) } )
3230, 31syl6eqr 2674 . . . . . . 7 |- ( ( ( J e. Comp /\ S e. ( Clsd ` J ) ) /\ s C_ J /\ S C_ U. s ) -> U. J = U. ( s u. { ( U. J \ S ) } ) )
334cmpcov 21192 . . . . . . 7 |- ( ( 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 )
342, 9, 32, 33syl3anc 1326 . . . . . 6 |- ( ( ( 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 8268 . . . . . . . 8 |- ( u e. ( ~P ( s u. { ( U. J \ S ) } ) i^i Fin ) <-> ( u C_ ( s u. { ( U. J \ S ) } ) /\ u e. Fin ) )
36 simp2l 1087 . . . . . . . . . . . 12 |- ( ( ( ( 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 3757 . . . . . . . . . . . 12 |- ( s u. { ( U. J \ S ) } ) = ( { ( U. J \ S ) } u. s )
3836, 37syl6sseq 3651 . . . . . . . . . . 11 |- ( ( ( ( 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 4052 . . . . . . . . . . 11 |- ( u C_ ( { ( U. J \ S ) } u. s ) <-> ( u \ { ( U. J \ S ) } ) C_ s )
4038, 39sylib 208 . . . . . . . . . 10 |- ( ( ( ( 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 8192 . . . . . . . . . . . 12 |- ( u e. Fin -> ( u \ { ( U. J \ S ) } ) e. Fin )
4241ad2antll 765 . . . . . . . . . . 11 |- ( ( ( ( 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 )
43423adant3 1081 . . . . . . . . . 10 |- ( ( ( ( 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 8268 . . . . . . . . . 10 |- ( ( u \ { ( U. J \ S ) } ) e. ( ~P s i^i Fin ) <-> ( ( u \ { ( U. J \ S ) } ) C_ s /\ ( u \ { ( U. J \ S ) } ) e. Fin ) )
4540, 43, 44sylanbrc 698 . . . . . . . . 9 |- ( ( ( ( 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 ) )
46103ad2ant1 1082 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
47123ad2ant1 1082 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 1063 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
4947, 48sseqtrd 3641 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
5046, 49sstrd 3613 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
5150sselda 3603 . . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 4439 . . . . . . . . . . . . . 14 |- ( v e. U. u <-> E. w ( v e. w /\ w e. u ) )
5351, 52sylib 208 . . . . . . . . . . . . 13 |- ( ( ( ( ( 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 473 . . . . . . . . . . . . . . . 16 |- ( ( v e. w /\ w e. u ) -> v e. w )
5554a1i 11 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 477 . . . . . . . . . . . . . . . . . 18 |- ( ( v e. w /\ w e. u ) -> w e. u )
5756a1i 11 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 3734 . . . . . . . . . . . . . . . . . . . . . 22 |- ( v e. S -> -. v e. ( U. J \ S ) )
5958ad2antlr 763 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( 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 2690 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( w = ( U. J \ S ) -> ( v e. w <-> v e. ( U. J \ S ) ) )
6160biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( w = ( U. J \ S ) -> ( v e. w -> v e. ( U. J \ S ) ) )
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( 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 ) ) ) )
6362com23 86 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( 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 ) ) ) )
6463imp 445 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( 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 ) ) )
6559, 64mtod 189 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( 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 ) )
6665ex 450 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 ) ) )
6766adantrd 484 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 4193 . . . . . . . . . . . . . . . . . . 19 |- ( w e. { ( U. J \ S ) } <-> w = ( U. J \ S ) )
6968notbii 310 . . . . . . . . . . . . . . . . . 18 |- ( -. w e. { ( U. J \ S ) } <-> -. w = ( U. J \ S ) )
7067, 69syl6ibr 242 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) } ) )
7157, 70jcad 555 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 3584 . . . . . . . . . . . . . . . 16 |- ( w e. ( u \ { ( U. J \ S ) } ) <-> ( w e. u /\ -. w e. { ( U. J \ S ) } ) )
7371, 72syl6ibr 242 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) } ) ) )
7455, 73jcad 555 . . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 ) } ) ) ) )
7574eximdv 1846 . . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) } ) ) ) )
7653, 75mpd 15 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) } ) ) )
7776ex 450 . . . . . . . . . . 11 |- ( ( ( ( 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 4439 . . . . . . . . . . 11 |- ( v e. U. ( u \ { ( U. J \ S ) } ) <-> E. w ( v e. w /\ w e. ( u \ { ( U. J \ S ) } ) ) )
7977, 78syl6ibr 242 . . . . . . . . . 10 |- ( ( ( ( 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 ) } ) ) )
8079ssrdv 3609 . . . . . . . . 9 |- ( ( ( ( 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 4444 . . . . . . . . . . 11 |- ( t = ( u \ { ( U. J \ S ) } ) -> U. t = U. ( u \ { ( U. J \ S ) } ) )
8281sseq2d 3633 . . . . . . . . . 10 |- ( t = ( u \ { ( U. J \ S ) } ) -> ( S C_ U. t <-> S C_ U. ( u \ { ( U. J \ S ) } ) ) )
8382rspcev 3309 . . . . . . . . 9 |- ( ( ( 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 )
8445, 80, 83syl2anc 693 . . . . . . . 8 |- ( ( ( ( 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 )
8535, 84syl3an2b 1363 . . . . . . 7 |- ( ( ( ( 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 )
8685rexlimdv3a 3033 . . . . . 6 |- ( ( ( 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 ) )
8734, 86mpd 15 . . . . 5 |- ( ( ( 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 )
88873exp 1264 . . . 4 |- ( ( 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 ) ) )
891, 88syl5bi 232 . . 3 |- ( ( 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 ) ) )
9089ralrimiv 2965 . 2 |- ( ( 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 21198 . . 3 |- ( J e. Comp -> J e. Top )
924cldss 20833 . . 3 |- ( S e. ( Clsd ` J ) -> S C_ U. J )
934cmpsub 21203 . . 3 |- ( ( 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 ) ) )
9491, 92, 93syl2an 494 . 2 |- ( ( 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 ) ) )
9590, 94mpbird 247 1 |- ( ( J e. Comp /\ S e. ( Clsd ` J ) ) -> ( J ↾t S ) e. Comp )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   {csn 4177   U.cuni 4436   ` cfv 5888  (class class class)co 6650   Fincfn 7955   ↾t crest 16081   Topctop 20698   Clsdccld 20820   Compccmp 21189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-fin 7959  df-fi 8317  df-rest 16083  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-cmp 21190
This theorem is referenced by:  hausllycmp  21297  cldllycmp  21298  txkgen  21455  cmphaushmeo  21603  cnheiborlem  22753  cmpcmet  23116  stoweidlem28  40245  stoweidlem50  40267  stoweidlem57  40274
  Copyright terms: Public domain W3C validator