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 \in V \land F : A ⟶ Comp) \to \prod_{𝑡} (F) \in Comp$

Proof

Step	Hyp	Ref	Expression
1		fvex	$⊢ \prod_{𝑡} (F) \in V$
2	1	uniex	$⊢ ⋃ \prod_{𝑡} (F) \in V$
3		axac3	$⊢ CHOICE$
4		acufl	$⊢ CHOICE \to UFL = V$
5	3 4	ax-mp	$⊢ UFL = V$
6	2 5	eleqtrri	$⊢ ⋃ \prod_{𝑡} (F) \in UFL$
7		cardeqv	$⊢ dom card = V$
8	2 7	eleqtrri	$⊢ ⋃ \prod_{𝑡} (F) \in dom card$
9	6 8	elini	$⊢ ⋃ \prod_{𝑡} (F) \in (UFL \cap dom card)$
10		eqid	$⊢ \prod_{𝑡} (F) = \prod_{𝑡} (F)$
11		eqid	$⊢ ⋃ \prod_{𝑡} (F) = ⋃ \prod_{𝑡} (F)$
12	10 11	ptcmpg	$⊢ (A \in V \land F : A ⟶ Comp \land ⋃ \prod_{𝑡} (F) \in (UFL \cap dom card)) \to \prod_{𝑡} (F) \in Comp$
13	9 12	mp3an3	$⊢ (A \in V \land F : A ⟶ Comp) \to \prod_{𝑡} (F) \in Comp$