Metamath Proof Explorer

Theorem ptcmpfi

Description: A topological product of finitely many compact spaces is compact. This weak version of Tychonoff's theorem does not require the axiom of choice. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Assertion ptcmpfi 
|- ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` F ) e. Comp )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> Comp -> F Fn A )
2 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
3 1 2 syl 
 |-  ( F : A --> Comp -> ( F |` A ) = F )
4 3 adantl 
 |-  ( ( A e. Fin /\ F : A --> Comp ) -> ( F |` A ) = F )
5 4 fveq2d 
 |-  ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` A ) ) = ( Xt_ ` F ) )
6 ssid 
 |-  A C_ A
7 sseq1 
 |-  ( x = (/) -> ( x C_ A <-> (/) C_ A ) )
8 reseq2 
 |-  ( x = (/) -> ( F |` x ) = ( F |` (/) ) )
9 res0 
 |-  ( F |` (/) ) = (/)
10 8 9 eqtrdi 
 |-  ( x = (/) -> ( F |` x ) = (/) )
11 10 fveq2d 
 |-  ( x = (/) -> ( Xt_ ` ( F |` x ) ) = ( Xt_ ` (/) ) )
12 11 eleq1d 
 |-  ( x = (/) -> ( ( Xt_ ` ( F |` x ) ) e. Comp <-> ( Xt_ ` (/) ) e. Comp ) )
13 12 imbi2d 
 |-  ( x = (/) -> ( ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` x ) ) e. Comp ) <-> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` (/) ) e. Comp ) ) )
14 7 13 imbi12d 
 |-  ( x = (/) -> ( ( x C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` x ) ) e. Comp ) ) <-> ( (/) C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` (/) ) e. Comp ) ) ) )
15 sseq1 
 |-  ( x = y -> ( x C_ A <-> y C_ A ) )
16 reseq2 
 |-  ( x = y -> ( F |` x ) = ( F |` y ) )
17 16 fveq2d 
 |-  ( x = y -> ( Xt_ ` ( F |` x ) ) = ( Xt_ ` ( F |` y ) ) )
18 17 eleq1d 
 |-  ( x = y -> ( ( Xt_ ` ( F |` x ) ) e. Comp <-> ( Xt_ ` ( F |` y ) ) e. Comp ) )
19 18 imbi2d 
 |-  ( x = y -> ( ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` x ) ) e. Comp ) <-> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` y ) ) e. Comp ) ) )
20 15 19 imbi12d 
 |-  ( x = y -> ( ( x C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` x ) ) e. Comp ) ) <-> ( y C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` y ) ) e. Comp ) ) ) )
21 sseq1 
 |-  ( x = ( y u. { z } ) -> ( x C_ A <-> ( y u. { z } ) C_ A ) )
22 reseq2 
 |-  ( x = ( y u. { z } ) -> ( F |` x ) = ( F |` ( y u. { z } ) ) )
23 22 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( Xt_ ` ( F |` x ) ) = ( Xt_ ` ( F |` ( y u. { z } ) ) ) )
24 23 eleq1d 
 |-  ( x = ( y u. { z } ) -> ( ( Xt_ ` ( F |` x ) ) e. Comp <-> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) )
25 24 imbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` x ) ) e. Comp ) <-> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) ) )
26 21 25 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( x C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` x ) ) e. Comp ) ) <-> ( ( y u. { z } ) C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) ) ) )
27 sseq1 
 |-  ( x = A -> ( x C_ A <-> A C_ A ) )
28 reseq2 
 |-  ( x = A -> ( F |` x ) = ( F |` A ) )
29 28 fveq2d 
 |-  ( x = A -> ( Xt_ ` ( F |` x ) ) = ( Xt_ ` ( F |` A ) ) )
30 29 eleq1d 
 |-  ( x = A -> ( ( Xt_ ` ( F |` x ) ) e. Comp <-> ( Xt_ ` ( F |` A ) ) e. Comp ) )
31 30 imbi2d 
 |-  ( x = A -> ( ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` x ) ) e. Comp ) <-> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` A ) ) e. Comp ) ) )
32 27 31 imbi12d 
 |-  ( x = A -> ( ( x C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` x ) ) e. Comp ) ) <-> ( A C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` A ) ) e. Comp ) ) ) )
33 0ex 
 |-  (/) e. _V
34 f0 
 |-  (/) : (/) --> Top
35 pttop 
 |-  ( ( (/) e. _V /\ (/) : (/) --> Top ) -> ( Xt_ ` (/) ) e. Top )
36 33 34 35 mp2an 
 |-  ( Xt_ ` (/) ) e. Top
37 eqid 
 |-  ( Xt_ ` (/) ) = ( Xt_ ` (/) )
38 37 ptuni 
 |-  ( ( (/) e. _V /\ (/) : (/) --> Top ) -> X_ x e. (/) U. ( (/) ` x ) = U. ( Xt_ ` (/) ) )
39 33 34 38 mp2an 
 |-  X_ x e. (/) U. ( (/) ` x ) = U. ( Xt_ ` (/) )
40 ixp0x 
 |-  X_ x e. (/) U. ( (/) ` x ) = { (/) }
41 snfi 
 |-  { (/) } e. Fin
42 40 41 eqeltri 
 |-  X_ x e. (/) U. ( (/) ` x ) e. Fin
43 39 42 eqeltrri 
 |-  U. ( Xt_ ` (/) ) e. Fin
44 pwfi 
 |-  ( U. ( Xt_ ` (/) ) e. Fin <-> ~P U. ( Xt_ ` (/) ) e. Fin )
45 43 44 mpbi 
 |-  ~P U. ( Xt_ ` (/) ) e. Fin
46 pwuni 
 |-  ( Xt_ ` (/) ) C_ ~P U. ( Xt_ ` (/) )
47 ssfi 
 |-  ( ( ~P U. ( Xt_ ` (/) ) e. Fin /\ ( Xt_ ` (/) ) C_ ~P U. ( Xt_ ` (/) ) ) -> ( Xt_ ` (/) ) e. Fin )
48 45 46 47 mp2an 
 |-  ( Xt_ ` (/) ) e. Fin
49 36 48 elini 
 |-  ( Xt_ ` (/) ) e. ( Top i^i Fin )
50 fincmp 
 |-  ( ( Xt_ ` (/) ) e. ( Top i^i Fin ) -> ( Xt_ ` (/) ) e. Comp )
51 49 50 ax-mp 
 |-  ( Xt_ ` (/) ) e. Comp
52 51 2a1i 
 |-  ( (/) C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` (/) ) e. Comp ) )
53 ssun1 
 |-  y C_ ( y u. { z } )
54 id 
 |-  ( ( y u. { z } ) C_ A -> ( y u. { z } ) C_ A )
55 53 54 sstrid 
 |-  ( ( y u. { z } ) C_ A -> y C_ A )
56 55 imim1i 
 |-  ( ( y C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` y ) ) e. Comp ) ) -> ( ( y u. { z } ) C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` y ) ) e. Comp ) ) )
57 eqid 
 |-  U. ( Xt_ ` ( F |` y ) ) = U. ( Xt_ ` ( F |` y ) )
58 eqid 
 |-  U. ( Xt_ ` ( F |` { z } ) ) = U. ( Xt_ ` ( F |` { z } ) )
59 eqid 
 |-  ( Xt_ ` ( F |` ( y u. { z } ) ) ) = ( Xt_ ` ( F |` ( y u. { z } ) ) )
60 resabs1 
 |-  ( y C_ ( y u. { z } ) -> ( ( F |` ( y u. { z } ) ) |` y ) = ( F |` y ) )
61 53 60 ax-mp 
 |-  ( ( F |` ( y u. { z } ) ) |` y ) = ( F |` y )
62 61 eqcomi 
 |-  ( F |` y ) = ( ( F |` ( y u. { z } ) ) |` y )
63 62 fveq2i 
 |-  ( Xt_ ` ( F |` y ) ) = ( Xt_ ` ( ( F |` ( y u. { z } ) ) |` y ) )
64 ssun2 
 |-  { z } C_ ( y u. { z } )
65 resabs1 
 |-  ( { z } C_ ( y u. { z } ) -> ( ( F |` ( y u. { z } ) ) |` { z } ) = ( F |` { z } ) )
66 64 65 ax-mp 
 |-  ( ( F |` ( y u. { z } ) ) |` { z } ) = ( F |` { z } )
67 66 eqcomi 
 |-  ( F |` { z } ) = ( ( F |` ( y u. { z } ) ) |` { z } )
68 67 fveq2i 
 |-  ( Xt_ ` ( F |` { z } ) ) = ( Xt_ ` ( ( F |` ( y u. { z } ) ) |` { z } ) )
69 eqid 
 |-  ( u e. U. ( Xt_ ` ( F |` y ) ) , v e. U. ( Xt_ ` ( F |` { z } ) ) |-> ( u u. v ) ) = ( u e. U. ( Xt_ ` ( F |` y ) ) , v e. U. ( Xt_ ` ( F |` { z } ) ) |-> ( u u. v ) )
70 vex 
 |-  y e. _V
71 snex 
 |-  { z } e. _V
72 70 71 unex 
 |-  ( y u. { z } ) e. _V
73 72 a1i 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( y u. { z } ) e. _V )
74 simplr 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> F : A --> Comp )
75 cmptop 
 |-  ( x e. Comp -> x e. Top )
76 75 ssriv 
 |-  Comp C_ Top
77 fss 
 |-  ( ( F : A --> Comp /\ Comp C_ Top ) -> F : A --> Top )
78 74 76 77 sylancl 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> F : A --> Top )
79 simprr 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( y u. { z } ) C_ A )
80 78 79 fssresd 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( F |` ( y u. { z } ) ) : ( y u. { z } ) --> Top )
81 eqidd 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( y u. { z } ) = ( y u. { z } ) )
82 simprl 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> -. z e. y )
83 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
84 82 83 sylibr 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( y i^i { z } ) = (/) )
85 57 58 59 63 68 69 73 80 81 84 ptunhmeo 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( u e. U. ( Xt_ ` ( F |` y ) ) , v e. U. ( Xt_ ` ( F |` { z } ) ) |-> ( u u. v ) ) e. ( ( ( Xt_ ` ( F |` y ) ) tX ( Xt_ ` ( F |` { z } ) ) ) Homeo ( Xt_ ` ( F |` ( y u. { z } ) ) ) ) )
86 hmphi 
 |-  ( ( u e. U. ( Xt_ ` ( F |` y ) ) , v e. U. ( Xt_ ` ( F |` { z } ) ) |-> ( u u. v ) ) e. ( ( ( Xt_ ` ( F |` y ) ) tX ( Xt_ ` ( F |` { z } ) ) ) Homeo ( Xt_ ` ( F |` ( y u. { z } ) ) ) ) -> ( ( Xt_ ` ( F |` y ) ) tX ( Xt_ ` ( F |` { z } ) ) ) ~= ( Xt_ ` ( F |` ( y u. { z } ) ) ) )
87 85 86 syl 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( ( Xt_ ` ( F |` y ) ) tX ( Xt_ ` ( F |` { z } ) ) ) ~= ( Xt_ ` ( F |` ( y u. { z } ) ) ) )
88 1 ad2antlr 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> F Fn A )
89 64 79 sstrid 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> { z } C_ A )
90 vex 
 |-  z e. _V
91 90 snss 
 |-  ( z e. A <-> { z } C_ A )
92 89 91 sylibr 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> z e. A )
93 fnressn 
 |-  ( ( F Fn A /\ z e. A ) -> ( F |` { z } ) = { <. z , ( F ` z ) >. } )
94 88 92 93 syl2anc 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( F |` { z } ) = { <. z , ( F ` z ) >. } )
95 94 fveq2d 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( Xt_ ` ( F |` { z } ) ) = ( Xt_ ` { <. z , ( F ` z ) >. } ) )
96 eqid 
 |-  ( Xt_ ` { <. z , ( F ` z ) >. } ) = ( Xt_ ` { <. z , ( F ` z ) >. } )
97 90 a1i 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> z e. _V )
98 74 92 ffvelrnd 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( F ` z ) e. Comp )
99 76 98 sselid 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( F ` z ) e. Top )
100 toptopon2 
 |-  ( ( F ` z ) e. Top <-> ( F ` z ) e. ( TopOn ` U. ( F ` z ) ) )
101 99 100 sylib 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( F ` z ) e. ( TopOn ` U. ( F ` z ) ) )
102 96 97 101 pt1hmeo 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( x e. U. ( F ` z ) |-> { <. z , x >. } ) e. ( ( F ` z ) Homeo ( Xt_ ` { <. z , ( F ` z ) >. } ) ) )
103 hmphi 
 |-  ( ( x e. U. ( F ` z ) |-> { <. z , x >. } ) e. ( ( F ` z ) Homeo ( Xt_ ` { <. z , ( F ` z ) >. } ) ) -> ( F ` z ) ~= ( Xt_ ` { <. z , ( F ` z ) >. } ) )
104 102 103 syl 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( F ` z ) ~= ( Xt_ ` { <. z , ( F ` z ) >. } ) )
105 cmphmph 
 |-  ( ( F ` z ) ~= ( Xt_ ` { <. z , ( F ` z ) >. } ) -> ( ( F ` z ) e. Comp -> ( Xt_ ` { <. z , ( F ` z ) >. } ) e. Comp ) )
106 104 98 105 sylc 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( Xt_ ` { <. z , ( F ` z ) >. } ) e. Comp )
107 95 106 eqeltrd 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( Xt_ ` ( F |` { z } ) ) e. Comp )
108 txcmp 
 |-  ( ( ( Xt_ ` ( F |` y ) ) e. Comp /\ ( Xt_ ` ( F |` { z } ) ) e. Comp ) -> ( ( Xt_ ` ( F |` y ) ) tX ( Xt_ ` ( F |` { z } ) ) ) e. Comp )
109 108 expcom 
 |-  ( ( Xt_ ` ( F |` { z } ) ) e. Comp -> ( ( Xt_ ` ( F |` y ) ) e. Comp -> ( ( Xt_ ` ( F |` y ) ) tX ( Xt_ ` ( F |` { z } ) ) ) e. Comp ) )
110 107 109 syl 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( ( Xt_ ` ( F |` y ) ) e. Comp -> ( ( Xt_ ` ( F |` y ) ) tX ( Xt_ ` ( F |` { z } ) ) ) e. Comp ) )
111 cmphmph 
 |-  ( ( ( Xt_ ` ( F |` y ) ) tX ( Xt_ ` ( F |` { z } ) ) ) ~= ( Xt_ ` ( F |` ( y u. { z } ) ) ) -> ( ( ( Xt_ ` ( F |` y ) ) tX ( Xt_ ` ( F |` { z } ) ) ) e. Comp -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) )
112 87 110 111 sylsyld 
 |-  ( ( ( A e. Fin /\ F : A --> Comp ) /\ ( -. z e. y /\ ( y u. { z } ) C_ A ) ) -> ( ( Xt_ ` ( F |` y ) ) e. Comp -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) )
113 112 expcom 
 |-  ( ( -. z e. y /\ ( y u. { z } ) C_ A ) -> ( ( A e. Fin /\ F : A --> Comp ) -> ( ( Xt_ ` ( F |` y ) ) e. Comp -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) ) )
114 113 a2d 
 |-  ( ( -. z e. y /\ ( y u. { z } ) C_ A ) -> ( ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` y ) ) e. Comp ) -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) ) )
115 114 ex 
 |-  ( -. z e. y -> ( ( y u. { z } ) C_ A -> ( ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` y ) ) e. Comp ) -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) ) ) )
116 115 a2d 
 |-  ( -. z e. y -> ( ( ( y u. { z } ) C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` y ) ) e. Comp ) ) -> ( ( y u. { z } ) C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) ) ) )
117 56 116 syl5 
 |-  ( -. z e. y -> ( ( y C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` y ) ) e. Comp ) ) -> ( ( y u. { z } ) C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) ) ) )
118 117 adantl 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( y C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` y ) ) e. Comp ) ) -> ( ( y u. { z } ) C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` ( y u. { z } ) ) ) e. Comp ) ) ) )
119 14 20 26 32 52 118 findcard2s 
 |-  ( A e. Fin -> ( A C_ A -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` A ) ) e. Comp ) ) )
120 6 119 mpi 
 |-  ( A e. Fin -> ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` A ) ) e. Comp ) )
121 120 anabsi5 
 |-  ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` ( F |` A ) ) e. Comp )
122 5 121 eqeltrrd 
 |-  ( ( A e. Fin /\ F : A --> Comp ) -> ( Xt_ ` F ) e. Comp )