Metamath Proof Explorer


Theorem fiuncmp

Description: A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypothesis fiuncmp.1 X = J
Assertion fiuncmp J Top A Fin x A J 𝑡 B Comp J 𝑡 x A B Comp

Proof

Step Hyp Ref Expression
1 fiuncmp.1 X = J
2 ssid A A
3 simp2 J Top A Fin x A J 𝑡 B Comp A Fin
4 sseq1 t = t A A
5 iuneq1 t = x t B = x B
6 0iun x B =
7 5 6 eqtrdi t = x t B =
8 7 oveq2d t = J 𝑡 x t B = J 𝑡
9 8 eleq1d t = J 𝑡 x t B Comp J 𝑡 Comp
10 4 9 imbi12d t = t A J 𝑡 x t B Comp A J 𝑡 Comp
11 10 imbi2d t = J Top A Fin x A J 𝑡 B Comp t A J 𝑡 x t B Comp J Top A Fin x A J 𝑡 B Comp A J 𝑡 Comp
12 sseq1 t = y t A y A
13 iuneq1 t = y x t B = x y B
14 13 oveq2d t = y J 𝑡 x t B = J 𝑡 x y B
15 14 eleq1d t = y J 𝑡 x t B Comp J 𝑡 x y B Comp
16 12 15 imbi12d t = y t A J 𝑡 x t B Comp y A J 𝑡 x y B Comp
17 16 imbi2d t = y J Top A Fin x A J 𝑡 B Comp t A J 𝑡 x t B Comp J Top A Fin x A J 𝑡 B Comp y A J 𝑡 x y B Comp
18 sseq1 t = y z t A y z A
19 iuneq1 t = y z x t B = x y z B
20 19 oveq2d t = y z J 𝑡 x t B = J 𝑡 x y z B
21 20 eleq1d t = y z J 𝑡 x t B Comp J 𝑡 x y z B Comp
22 18 21 imbi12d t = y z t A J 𝑡 x t B Comp y z A J 𝑡 x y z B Comp
23 22 imbi2d t = y z J Top A Fin x A J 𝑡 B Comp t A J 𝑡 x t B Comp J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y z B Comp
24 sseq1 t = A t A A A
25 iuneq1 t = A x t B = x A B
26 25 oveq2d t = A J 𝑡 x t B = J 𝑡 x A B
27 26 eleq1d t = A J 𝑡 x t B Comp J 𝑡 x A B Comp
28 24 27 imbi12d t = A t A J 𝑡 x t B Comp A A J 𝑡 x A B Comp
29 28 imbi2d t = A J Top A Fin x A J 𝑡 B Comp t A J 𝑡 x t B Comp J Top A Fin x A J 𝑡 B Comp A A J 𝑡 x A B Comp
30 rest0 J Top J 𝑡 =
31 0cmp Comp
32 30 31 eqeltrdi J Top J 𝑡 Comp
33 32 3ad2ant1 J Top A Fin x A J 𝑡 B Comp J 𝑡 Comp
34 33 a1d J Top A Fin x A J 𝑡 B Comp A J 𝑡 Comp
35 ssun1 y y z
36 id y z A y z A
37 35 36 sstrid y z A y A
38 37 imim1i y A J 𝑡 x y B Comp y z A J 𝑡 x y B Comp
39 simpl1 J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J Top
40 iunxun x y z B = x y B x z B
41 simprr J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y B Comp
42 cmptop J 𝑡 x y B Comp J 𝑡 x y B Top
43 restrcl J 𝑡 x y B Top J V x y B V
44 43 simprd J 𝑡 x y B Top x y B V
45 41 42 44 3syl J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp x y B V
46 nfcv _ t B
47 nfcsb1v _ x t / x B
48 csbeq1a x = t B = t / x B
49 46 47 48 cbviun x z B = t z t / x B
50 vex z V
51 csbeq1 t = z t / x B = z / x B
52 50 51 iunxsn t z t / x B = z / x B
53 49 52 eqtri x z B = z / x B
54 51 oveq2d t = z J 𝑡 t / x B = J 𝑡 z / x B
55 54 eleq1d t = z J 𝑡 t / x B Comp J 𝑡 z / x B Comp
56 simpl3 J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp x A J 𝑡 B Comp
57 nfv t J 𝑡 B Comp
58 nfcv _ x J
59 nfcv _ x 𝑡
60 58 59 47 nfov _ x J 𝑡 t / x B
61 60 nfel1 x J 𝑡 t / x B Comp
62 48 oveq2d x = t J 𝑡 B = J 𝑡 t / x B
63 62 eleq1d x = t J 𝑡 B Comp J 𝑡 t / x B Comp
64 57 61 63 cbvralw x A J 𝑡 B Comp t A J 𝑡 t / x B Comp
65 56 64 sylib J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp t A J 𝑡 t / x B Comp
66 ssun2 z y z
67 simprl J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp y z A
68 66 67 sstrid J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp z A
69 50 snss z A z A
70 68 69 sylibr J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp z A
71 55 65 70 rspcdva J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 z / x B Comp
72 cmptop J 𝑡 z / x B Comp J 𝑡 z / x B Top
73 restrcl J 𝑡 z / x B Top J V z / x B V
74 73 simprd J 𝑡 z / x B Top z / x B V
75 71 72 74 3syl J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp z / x B V
76 53 75 eqeltrid J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp x z B V
77 unexg x y B V x z B V x y B x z B V
78 45 76 77 syl2anc J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp x y B x z B V
79 40 78 eqeltrid J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp x y z B V
80 resttop J Top x y z B V J 𝑡 x y z B Top
81 39 79 80 syl2anc J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B Top
82 eqid J = J
83 82 restin J Top x y z B V J 𝑡 x y z B = J 𝑡 x y z B J
84 39 79 83 syl2anc J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B = J 𝑡 x y z B J
85 84 unieqd J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B = J 𝑡 x y z B J
86 inss2 x y z B J J
87 86 1 sseqtrri x y z B J X
88 1 restuni J Top x y z B J X x y z B J = J 𝑡 x y z B J
89 39 87 88 sylancl J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp x y z B J = J 𝑡 x y z B J
90 85 89 eqtr4d J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B = x y z B J
91 53 uneq2i x y B x z B = x y B z / x B
92 40 91 eqtri x y z B = x y B z / x B
93 92 ineq1i x y z B J = x y B z / x B J
94 indir x y B z / x B J = x y B J z / x B J
95 93 94 eqtri x y z B J = x y B J z / x B J
96 90 95 eqtrdi J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B = x y B J z / x B J
97 inss1 x y B J x y B
98 ssun1 x y B x y B x z B
99 98 40 sseqtrri x y B x y z B
100 97 99 sstri x y B J x y z B
101 100 a1i J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp x y B J x y z B
102 restabs J Top x y B J x y z B x y z B V J 𝑡 x y z B 𝑡 x y B J = J 𝑡 x y B J
103 39 101 79 102 syl3anc J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B 𝑡 x y B J = J 𝑡 x y B J
104 82 restin J Top x y B V J 𝑡 x y B = J 𝑡 x y B J
105 39 45 104 syl2anc J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y B = J 𝑡 x y B J
106 103 105 eqtr4d J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B 𝑡 x y B J = J 𝑡 x y B
107 106 41 eqeltrd J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B 𝑡 x y B J Comp
108 inss1 z / x B J z / x B
109 ssun2 x z B x y B x z B
110 109 40 sseqtrri x z B x y z B
111 53 110 eqsstrri z / x B x y z B
112 108 111 sstri z / x B J x y z B
113 112 a1i J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp z / x B J x y z B
114 restabs J Top z / x B J x y z B x y z B V J 𝑡 x y z B 𝑡 z / x B J = J 𝑡 z / x B J
115 39 113 79 114 syl3anc J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B 𝑡 z / x B J = J 𝑡 z / x B J
116 82 restin J Top z / x B V J 𝑡 z / x B = J 𝑡 z / x B J
117 39 75 116 syl2anc J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 z / x B = J 𝑡 z / x B J
118 115 117 eqtr4d J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B 𝑡 z / x B J = J 𝑡 z / x B
119 118 71 eqeltrd J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B 𝑡 z / x B J Comp
120 eqid J 𝑡 x y z B = J 𝑡 x y z B
121 120 uncmp J 𝑡 x y z B Top J 𝑡 x y z B = x y B J z / x B J J 𝑡 x y z B 𝑡 x y B J Comp J 𝑡 x y z B 𝑡 z / x B J Comp J 𝑡 x y z B Comp
122 81 96 107 119 121 syl22anc J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B Comp
123 122 exp32 J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp J 𝑡 x y z B Comp
124 123 a2d J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y B Comp y z A J 𝑡 x y z B Comp
125 38 124 syl5 J Top A Fin x A J 𝑡 B Comp y A J 𝑡 x y B Comp y z A J 𝑡 x y z B Comp
126 125 a2i J Top A Fin x A J 𝑡 B Comp y A J 𝑡 x y B Comp J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y z B Comp
127 126 a1i y Fin J Top A Fin x A J 𝑡 B Comp y A J 𝑡 x y B Comp J Top A Fin x A J 𝑡 B Comp y z A J 𝑡 x y z B Comp
128 11 17 23 29 34 127 findcard2 A Fin J Top A Fin x A J 𝑡 B Comp A A J 𝑡 x A B Comp
129 3 128 mpcom J Top A Fin x A J 𝑡 B Comp A A J 𝑡 x A B Comp
130 2 129 mpi J Top A Fin x A J 𝑡 B Comp J 𝑡 x A B Comp