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 )