Metamath Proof Explorer

Theorem uncmp

Description: The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010)

Ref Expression
Hypothesis uncmp.1 
|- X = U. J
Assertion uncmp 
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> J e. Comp )

Proof

Step Hyp Ref Expression
1 uncmp.1 
 |-  X = U. J
2 simpll 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> J e. Top )
3 simpll 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> J e. Top )
4 ssun1 
 |-  S C_ ( S u. T )
5 sseq2 
 |-  ( X = ( S u. T ) -> ( S C_ X <-> S C_ ( S u. T ) ) )
6 4 5 mpbiri 
 |-  ( X = ( S u. T ) -> S C_ X )
7 6 ad2antlr 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> S C_ X )
8 1 cmpsub 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( J |`t S ) e. Comp <-> A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) ) )
9 3 7 8 syl2anc 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( J |`t S ) e. Comp <-> A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) ) )
10 simprr 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> X = U. c )
11 7 10 sseqtrd 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> S C_ U. c )
12 unieq 
 |-  ( m = c -> U. m = U. c )
13 12 sseq2d 
 |-  ( m = c -> ( S C_ U. m <-> S C_ U. c ) )
14 pweq 
 |-  ( m = c -> ~P m = ~P c )
15 14 ineq1d 
 |-  ( m = c -> ( ~P m i^i Fin ) = ( ~P c i^i Fin ) )
16 15 rexeqdv 
 |-  ( m = c -> ( E. n e. ( ~P m i^i Fin ) S C_ U. n <-> E. n e. ( ~P c i^i Fin ) S C_ U. n ) )
17 13 16 imbi12d 
 |-  ( m = c -> ( ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) <-> ( S C_ U. c -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) ) )
18 17 rspcv 
 |-  ( c e. ~P J -> ( A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) -> ( S C_ U. c -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) ) )
19 18 ad2antrl 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) -> ( S C_ U. c -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) ) )
20 11 19 mpid 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) )
21 9 20 sylbid 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( J |`t S ) e. Comp -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) )
22 ssun2 
 |-  T C_ ( S u. T )
23 sseq2 
 |-  ( X = ( S u. T ) -> ( T C_ X <-> T C_ ( S u. T ) ) )
24 22 23 mpbiri 
 |-  ( X = ( S u. T ) -> T C_ X )
25 24 ad2antlr 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> T C_ X )
26 1 cmpsub 
 |-  ( ( J e. Top /\ T C_ X ) -> ( ( J |`t T ) e. Comp <-> A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) ) )
27 3 25 26 syl2anc 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( J |`t T ) e. Comp <-> A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) ) )
28 25 10 sseqtrd 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> T C_ U. c )
29 unieq 
 |-  ( r = c -> U. r = U. c )
30 29 sseq2d 
 |-  ( r = c -> ( T C_ U. r <-> T C_ U. c ) )
31 pweq 
 |-  ( r = c -> ~P r = ~P c )
32 31 ineq1d 
 |-  ( r = c -> ( ~P r i^i Fin ) = ( ~P c i^i Fin ) )
33 32 rexeqdv 
 |-  ( r = c -> ( E. s e. ( ~P r i^i Fin ) T C_ U. s <-> E. s e. ( ~P c i^i Fin ) T C_ U. s ) )
34 30 33 imbi12d 
 |-  ( r = c -> ( ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) <-> ( T C_ U. c -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) )
35 34 rspcv 
 |-  ( c e. ~P J -> ( A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) -> ( T C_ U. c -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) )
36 35 ad2antrl 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) -> ( T C_ U. c -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) )
37 28 36 mpid 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) )
38 27 37 sylbid 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( J |`t T ) e. Comp -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) )
39 reeanv 
 |-  ( E. n e. ( ~P c i^i Fin ) E. s e. ( ~P c i^i Fin ) ( S C_ U. n /\ T C_ U. s ) <-> ( E. n e. ( ~P c i^i Fin ) S C_ U. n /\ E. s e. ( ~P c i^i Fin ) T C_ U. s ) )
40 elinel1 
 |-  ( n e. ( ~P c i^i Fin ) -> n e. ~P c )
41 40 elpwid 
 |-  ( n e. ( ~P c i^i Fin ) -> n C_ c )
42 elinel1 
 |-  ( s e. ( ~P c i^i Fin ) -> s e. ~P c )
43 42 elpwid 
 |-  ( s e. ( ~P c i^i Fin ) -> s C_ c )
44 41 43 anim12i 
 |-  ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) -> ( n C_ c /\ s C_ c ) )
45 44 ad2antrl 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n C_ c /\ s C_ c ) )
46 unss 
 |-  ( ( n C_ c /\ s C_ c ) <-> ( n u. s ) C_ c )
47 45 46 sylib 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n u. s ) C_ c )
48 elinel2 
 |-  ( n e. ( ~P c i^i Fin ) -> n e. Fin )
49 elinel2 
 |-  ( s e. ( ~P c i^i Fin ) -> s e. Fin )
50 unfi 
 |-  ( ( n e. Fin /\ s e. Fin ) -> ( n u. s ) e. Fin )
51 48 49 50 syl2an 
 |-  ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) -> ( n u. s ) e. Fin )
52 51 ad2antrl 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n u. s ) e. Fin )
53 47 52 jca 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( ( n u. s ) C_ c /\ ( n u. s ) e. Fin ) )
54 elin 
 |-  ( ( n u. s ) e. ( ~P c i^i Fin ) <-> ( ( n u. s ) e. ~P c /\ ( n u. s ) e. Fin ) )
55 vex 
 |-  c e. _V
56 55 elpw2 
 |-  ( ( n u. s ) e. ~P c <-> ( n u. s ) C_ c )
57 56 anbi1i 
 |-  ( ( ( n u. s ) e. ~P c /\ ( n u. s ) e. Fin ) <-> ( ( n u. s ) C_ c /\ ( n u. s ) e. Fin ) )
58 54 57 bitr2i 
 |-  ( ( ( n u. s ) C_ c /\ ( n u. s ) e. Fin ) <-> ( n u. s ) e. ( ~P c i^i Fin ) )
59 53 58 sylib 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n u. s ) e. ( ~P c i^i Fin ) )
60 simpllr 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> X = ( S u. T ) )
61 ssun3 
 |-  ( S C_ U. n -> S C_ ( U. n u. U. s ) )
62 ssun4 
 |-  ( T C_ U. s -> T C_ ( U. n u. U. s ) )
63 61 62 anim12i 
 |-  ( ( S C_ U. n /\ T C_ U. s ) -> ( S C_ ( U. n u. U. s ) /\ T C_ ( U. n u. U. s ) ) )
64 63 ad2antll 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( S C_ ( U. n u. U. s ) /\ T C_ ( U. n u. U. s ) ) )
65 unss 
 |-  ( ( S C_ ( U. n u. U. s ) /\ T C_ ( U. n u. U. s ) ) <-> ( S u. T ) C_ ( U. n u. U. s ) )
66 64 65 sylib 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( S u. T ) C_ ( U. n u. U. s ) )
67 60 66 eqsstrd 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> X C_ ( U. n u. U. s ) )
68 uniun 
 |-  U. ( n u. s ) = ( U. n u. U. s )
69 67 68 sseqtrrdi 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> X C_ U. ( n u. s ) )
70 elpwi 
 |-  ( c e. ~P J -> c C_ J )
71 70 adantr 
 |-  ( ( c e. ~P J /\ X = U. c ) -> c C_ J )
72 71 ad2antlr 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> c C_ J )
73 47 72 sstrd 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n u. s ) C_ J )
74 uniss 
 |-  ( ( n u. s ) C_ J -> U. ( n u. s ) C_ U. J )
75 74 1 sseqtrrdi 
 |-  ( ( n u. s ) C_ J -> U. ( n u. s ) C_ X )
76 73 75 syl 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> U. ( n u. s ) C_ X )
77 69 76 eqssd 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> X = U. ( n u. s ) )
78 unieq 
 |-  ( d = ( n u. s ) -> U. d = U. ( n u. s ) )
79 78 rspceeqv 
 |-  ( ( ( n u. s ) e. ( ~P c i^i Fin ) /\ X = U. ( n u. s ) ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
80 59 77 79 syl2anc 
 |-  ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
81 80 exp32 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) -> ( ( S C_ U. n /\ T C_ U. s ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
82 81 rexlimdvv 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( E. n e. ( ~P c i^i Fin ) E. s e. ( ~P c i^i Fin ) ( S C_ U. n /\ T C_ U. s ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) )
83 39 82 syl5bir 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( E. n e. ( ~P c i^i Fin ) S C_ U. n /\ E. s e. ( ~P c i^i Fin ) T C_ U. s ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) )
84 21 38 83 syl2and 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) )
85 84 impancom 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> ( ( c e. ~P J /\ X = U. c ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) )
86 85 expd 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> ( c e. ~P J -> ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
87 86 ralrimiv 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) )
88 1 iscmp 
 |-  ( J e. Comp <-> ( J e. Top /\ A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
89 2 87 88 sylanbrc 
 |-  ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> J e. Comp )