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 )