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 )