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∈𝒫JS⊆⋃m→∃n∈𝒫m∩FinS⊆⋃n
9 3 7 8 syl2anc ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→J↾𝑡S∈Comp↔∀m∈𝒫JS⊆⋃m→∃n∈𝒫m∩FinS⊆⋃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∩FinS⊆⋃n↔∃n∈𝒫c∩FinS⊆⋃n
17 13 16 imbi12d ⊢m=c→S⊆⋃m→∃n∈𝒫m∩FinS⊆⋃n↔S⊆⋃c→∃n∈𝒫c∩FinS⊆⋃n
18 17 rspcv ⊢c∈𝒫J→∀m∈𝒫JS⊆⋃m→∃n∈𝒫m∩FinS⊆⋃n→S⊆⋃c→∃n∈𝒫c∩FinS⊆⋃n
19 18 ad2antrl ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→∀m∈𝒫JS⊆⋃m→∃n∈𝒫m∩FinS⊆⋃n→S⊆⋃c→∃n∈𝒫c∩FinS⊆⋃n
20 11 19 mpid ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→∀m∈𝒫JS⊆⋃m→∃n∈𝒫m∩FinS⊆⋃n→∃n∈𝒫c∩FinS⊆⋃n
21 9 20 sylbid ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→J↾𝑡S∈Comp→∃n∈𝒫c∩FinS⊆⋃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∈𝒫JT⊆⋃r→∃s∈𝒫r∩FinT⊆⋃s
27 3 25 26 syl2anc ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→J↾𝑡T∈Comp↔∀r∈𝒫JT⊆⋃r→∃s∈𝒫r∩FinT⊆⋃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∩FinT⊆⋃s↔∃s∈𝒫c∩FinT⊆⋃s
34 30 33 imbi12d ⊢r=c→T⊆⋃r→∃s∈𝒫r∩FinT⊆⋃s↔T⊆⋃c→∃s∈𝒫c∩FinT⊆⋃s
35 34 rspcv ⊢c∈𝒫J→∀r∈𝒫JT⊆⋃r→∃s∈𝒫r∩FinT⊆⋃s→T⊆⋃c→∃s∈𝒫c∩FinT⊆⋃s
36 35 ad2antrl ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→∀r∈𝒫JT⊆⋃r→∃s∈𝒫r∩FinT⊆⋃s→T⊆⋃c→∃s∈𝒫c∩FinT⊆⋃s
37 28 36 mpid ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→∀r∈𝒫JT⊆⋃r→∃s∈𝒫r∩FinT⊆⋃s→∃s∈𝒫c∩FinT⊆⋃s
38 27 37 sylbid ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→J↾𝑡T∈Comp→∃s∈𝒫c∩FinT⊆⋃s
39 reeanv ⊢∃n∈𝒫c∩Fin∃s∈𝒫c∩FinS⊆⋃n∧T⊆⋃s↔∃n∈𝒫c∩FinS⊆⋃n∧∃s∈𝒫c∩FinT⊆⋃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∩FinX=⋃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∩FinX=⋃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∩FinX=⋃d
82 81 rexlimdvv ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→∃n∈𝒫c∩Fin∃s∈𝒫c∩FinS⊆⋃n∧T⊆⋃s→∃d∈𝒫c∩FinX=⋃d
83 39 82 biimtrrid ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→∃n∈𝒫c∩FinS⊆⋃n∧∃s∈𝒫c∩FinT⊆⋃s→∃d∈𝒫c∩FinX=⋃d
84 21 38 83 syl2and ⊢J∈Top∧X=S∪T∧c∈𝒫J∧X=⋃c→J↾𝑡S∈Comp∧J↾𝑡T∈Comp→∃d∈𝒫c∩FinX=⋃d
85 84 impancom ⊢J∈Top∧X=S∪T∧J↾𝑡S∈Comp∧J↾𝑡T∈Comp→c∈𝒫J∧X=⋃c→∃d∈𝒫c∩FinX=⋃d
86 85 expd ⊢J∈Top∧X=S∪T∧J↾𝑡S∈Comp∧J↾𝑡T∈Comp→c∈𝒫J→X=⋃c→∃d∈𝒫c∩FinX=⋃d
87 86 ralrimiv ⊢J∈Top∧X=S∪T∧J↾𝑡S∈Comp∧J↾𝑡T∈Comp→∀c∈𝒫JX=⋃c→∃d∈𝒫c∩FinX=⋃d
88 1 iscmp ⊢J∈Comp↔J∈Top∧∀c∈𝒫JX=⋃c→∃d∈𝒫c∩FinX=⋃d
89 2 87 88 sylanbrc ⊢J∈Top∧X=S∪T∧J↾𝑡S∈Comp∧J↾𝑡T∈Comp→J∈Comp