ptcmpg

Description: Tychonoff's theorem: The product of compact spaces is compact. The choice principles needed are encoded in the last hypothesis: the base set of the product must be well-orderable and satisfy the ultrafilter lemma. Both these assumptions are satisfied if ~P ~P X is well-orderable, so if we assume the Axiom of Choice we can eliminate them (see ptcmp ). (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	ptcmpg.1	$⊢ J = \prod_{𝑡} (F)$
	ptcmpg.2	$⊢ X = ⋃ J$
Assertion	ptcmpg	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to J \in Comp$

Proof

Step	Hyp	Ref	Expression
1		ptcmpg.1	$⊢ J = \prod_{𝑡} (F)$
2		ptcmpg.2	$⊢ X = ⋃ J$
3		nfcv	$⊢ \underline{Ⅎ} k F (a)$
4		nfcv	$⊢ \underline{Ⅎ} a F (k)$
5		nfcv	$⊢ \underline{Ⅎ} k {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (a))}^{-1} [b]$
6		nfcv	$⊢ \underline{Ⅎ} u {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (a))}^{-1} [b]$
7		nfcv	$⊢ \underline{Ⅎ} a {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u]$
8		nfcv	$⊢ \underline{Ⅎ} b {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u]$
9		fveq2	$⊢ a = k \to F (a) = F (k)$
10		fveq2	$⊢ a = k \to w (a) = w (k)$
11	10	mpteq2dv	$⊢ a = k \to (w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (a)) = (w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))$
12	11	cnveqd	$⊢ a = k \to {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (a))}^{-1} = {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1}$
13	12	imaeq1d	$⊢ a = k \to {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (a))}^{-1} [b] = {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [b]$
14		imaeq2	$⊢ b = u \to {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [b] = {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u]$
15	13 14	sylan9eq	$⊢ (a = k \land b = u) \to {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (a))}^{-1} [b] = {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u]$
16	3 4 5 6 7 8 9 15	cbvmpox	$⊢ (a \in A, b \in F (a) ⟼ {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (a))}^{-1} [b]) = (k \in A, u \in F (k) ⟼ {(w \in \underset{n \in A}{⨉} ⋃ F (n) ⟼ w (k))}^{-1} [u])$
17		fveq2	$⊢ n = m \to F (n) = F (m)$
18	17	unieqd	$⊢ n = m \to ⋃ F (n) = ⋃ F (m)$
19	18	cbvixpv	$⊢ \underset{n \in A}{⨉} ⋃ F (n) = \underset{m \in A}{⨉} ⋃ F (m)$
20		simp1	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to A \in V$
21		simp2	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to F : A ⟶ Comp$
22		cmptop	$⊢ k \in Comp \to k \in Top$
23	22	ssriv	$⊢ Comp \subseteq Top$
24		fss	$⊢ (F : A ⟶ Comp \land Comp \subseteq Top) \to F : A ⟶ Top$
25	21 23 24	sylancl	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to F : A ⟶ Top$
26	1	ptuni	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{n \in A}{⨉} ⋃ F (n) = ⋃ J$
27	20 25 26	syl2anc	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to \underset{n \in A}{⨉} ⋃ F (n) = ⋃ J$
28	27 2	eqtr4di	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to \underset{n \in A}{⨉} ⋃ F (n) = X$
29		simp3	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to X \in (UFL \cap dom card)$
30	28 29	eqeltrd	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to \underset{n \in A}{⨉} ⋃ F (n) \in (UFL \cap dom card)$
31	16 19 20 21 30	ptcmplem5	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to \prod_{𝑡} (F) \in Comp$
32	1 31	eqeltrid	$⊢ (A \in V \land F : A ⟶ Comp \land X \in (UFL \cap dom card)) \to J \in Comp$

Metamath Proof Explorer

Theorem ptcmpg

Proof