# 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 sseldi
` |-  ( ( ( 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 )`