This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ 𝐹 ) ∈ Comp )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( ∏t ‘ 𝐹 ) ∈ V
2 1 uniex ⊢ ∪ ( ∏t ‘ 𝐹 ) ∈ V
3 axac3 ⊢ CHOICE
4 acufl ⊢ ( CHOICE → UFL = V )
5 3 4 ax-mp ⊢ UFL = V
6 2 5 eleqtrri ⊢ ∪ ( ∏t ‘ 𝐹 ) ∈ UFL
7 cardeqv ⊢ dom card = V
8 2 7 eleqtrri ⊢ ∪ ( ∏t ‘ 𝐹 ) ∈ dom card
9 6 8 elini ⊢ ∪ ( ∏t ‘ 𝐹 ) ∈ ( UFL ∩ dom card )
10 eqid ⊢ ( ∏t ‘ 𝐹 ) = ( ∏t ‘ 𝐹 )
11 eqid ⊢ ∪ ( ∏t ‘ 𝐹 ) = ∪ ( ∏t ‘ 𝐹 )
12 10 11 ptcmpg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ∧ ∪ ( ∏t ‘ 𝐹 ) ∈ ( UFL ∩ dom card ) ) → ( ∏t ‘ 𝐹 ) ∈ Comp )
13 9 12 mp3an3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ 𝐹 ) ∈ Comp )