Metamath Proof Explorer


Theorem 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 𝐽 = ( ∏t𝐹 )
ptcmpg.2 𝑋 = 𝐽
Assertion ptcmpg ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝐽 ∈ Comp )

Proof

Step Hyp Ref Expression
1 ptcmpg.1 𝐽 = ( ∏t𝐹 )
2 ptcmpg.2 𝑋 = 𝐽
3 nfcv 𝑘 ( 𝐹𝑎 )
4 nfcv 𝑎 ( 𝐹𝑘 )
5 nfcv 𝑘 ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑎 ) ) “ 𝑏 )
6 nfcv 𝑢 ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑎 ) ) “ 𝑏 )
7 nfcv 𝑎 ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 )
8 nfcv 𝑏 ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 )
9 fveq2 ( 𝑎 = 𝑘 → ( 𝐹𝑎 ) = ( 𝐹𝑘 ) )
10 fveq2 ( 𝑎 = 𝑘 → ( 𝑤𝑎 ) = ( 𝑤𝑘 ) )
11 10 mpteq2dv ( 𝑎 = 𝑘 → ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑎 ) ) = ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) )
12 11 cnveqd ( 𝑎 = 𝑘 ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑎 ) ) = ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) )
13 12 imaeq1d ( 𝑎 = 𝑘 → ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑎 ) ) “ 𝑏 ) = ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑏 ) )
14 imaeq2 ( 𝑏 = 𝑢 → ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑏 ) = ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) )
15 13 14 sylan9eq ( ( 𝑎 = 𝑘𝑏 = 𝑢 ) → ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑎 ) ) “ 𝑏 ) = ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) )
16 3 4 5 6 7 8 9 15 cbvmpox ( 𝑎𝐴 , 𝑏 ∈ ( 𝐹𝑎 ) ↦ ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑎 ) ) “ 𝑏 ) ) = ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤X 𝑛𝐴 ( 𝐹𝑛 ) ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) )
17 fveq2 ( 𝑛 = 𝑚 → ( 𝐹𝑛 ) = ( 𝐹𝑚 ) )
18 17 unieqd ( 𝑛 = 𝑚 ( 𝐹𝑛 ) = ( 𝐹𝑚 ) )
19 18 cbvixpv X 𝑛𝐴 ( 𝐹𝑛 ) = X 𝑚𝐴 ( 𝐹𝑚 )
20 simp1 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝐴𝑉 )
21 simp2 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝐹 : 𝐴 ⟶ Comp )
22 cmptop ( 𝑘 ∈ Comp → 𝑘 ∈ Top )
23 22 ssriv Comp ⊆ Top
24 fss ( ( 𝐹 : 𝐴 ⟶ Comp ∧ Comp ⊆ Top ) → 𝐹 : 𝐴 ⟶ Top )
25 21 23 24 sylancl ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝐹 : 𝐴 ⟶ Top )
26 1 ptuni ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → X 𝑛𝐴 ( 𝐹𝑛 ) = 𝐽 )
27 20 25 26 syl2anc ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → X 𝑛𝐴 ( 𝐹𝑛 ) = 𝐽 )
28 27 2 eqtr4di ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → X 𝑛𝐴 ( 𝐹𝑛 ) = 𝑋 )
29 simp3 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝑋 ∈ ( UFL ∩ dom card ) )
30 28 29 eqeltrd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → X 𝑛𝐴 ( 𝐹𝑛 ) ∈ ( UFL ∩ dom card ) )
31 16 19 20 21 30 ptcmplem5 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → ( ∏t𝐹 ) ∈ Comp )
32 1 31 eqeltrid ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Comp ∧ 𝑋 ∈ ( UFL ∩ dom card ) ) → 𝐽 ∈ Comp )