Metamath Proof Explorer

Theorem ptcmp

Description: Tychonoff's theorem: The product of compact spaces is compact. The proof uses the Axiom of Choice. (Contributed by Mario Carneiro, 26-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( Xt_ ` F ) e. _V
2 1 uniex 
 |-  U. ( Xt_ ` F ) e. _V
3 axac3 
 |-  CHOICE
4 acufl 
 |-  ( CHOICE -> UFL = _V )
5 3 4 ax-mp 
 |-  UFL = _V
6 2 5 eleqtrri 
 |-  U. ( Xt_ ` F ) e. UFL
7 cardeqv 
 |-  dom card = _V
8 2 7 eleqtrri 
 |-  U. ( Xt_ ` F ) e. dom card
9 6 8 elini 
 |-  U. ( Xt_ ` F ) e. ( UFL i^i dom card )
10 eqid 
 |-  ( Xt_ ` F ) = ( Xt_ ` F )
11 eqid 
 |-  U. ( Xt_ ` F ) = U. ( Xt_ ` F )
12 10 11 ptcmpg 
 |-  ( ( A e. V /\ F : A --> Comp /\ U. ( Xt_ ` F ) e. ( UFL i^i dom card ) ) -> ( Xt_ ` F ) e. Comp )
13 9 12 mp3an3 
 |-  ( ( A e. V /\ F : A --> Comp ) -> ( Xt_ ` F ) e. Comp )