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 = J
Assertion uncmp J Top X = S T J 𝑡 S Comp J 𝑡 T Comp J Comp

Proof

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