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 ∈ V ∧ F : A ⟶ Comp → ∏ 𝑡 ⁡ F ∈ Comp

Proof

Step Hyp Ref Expression
1 fvex ⊢ ∏ 𝑡 ⁡ F ∈ V
2 1 uniex ⊢ ⋃ ∏ 𝑡 ⁡ F ∈ V
3 axac3 ⊢ CHOICE
4 acufl ⊢ CHOICE → UFL = V
5 3 4 ax-mp ⊢ UFL = V
6 2 5 eleqtrri ⊢ ⋃ ∏ 𝑡 ⁡ F ∈ UFL
7 cardeqv ⊢ dom ⁡ card = V
8 2 7 eleqtrri ⊢ ⋃ ∏ 𝑡 ⁡ F ∈ dom ⁡ card
9 6 8 elini ⊢ ⋃ ∏ 𝑡 ⁡ F ∈ UFL ∩ dom ⁡ card
10 eqid ⊢ ∏ 𝑡 ⁡ F = ∏ 𝑡 ⁡ F
11 eqid ⊢ ⋃ ∏ 𝑡 ⁡ F = ⋃ ∏ 𝑡 ⁡ F
12 10 11 ptcmpg ⊢ A ∈ V ∧ F : A ⟶ Comp ∧ ⋃ ∏ 𝑡 ⁡ F ∈ UFL ∩ dom ⁡ card → ∏ 𝑡 ⁡ F ∈ Comp
13 9 12 mp3an3 ⊢ A ∈ V ∧ F : A ⟶ Comp → ∏ 𝑡 ⁡ F ∈ Comp