This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ptcn

Description: If every projection of a function is continuous, then the function itself is continuous into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Hypotheses ptcn.2 ⊢ 𝐾 = ( ∏t ‘ 𝐹 )
ptcn.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
ptcn.4 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
ptcn.5 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ Top )
ptcn.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) )
Assertion ptcn ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 ptcn.2 ⊢ 𝐾 = ( ∏t ‘ 𝐹 )
2 ptcn.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 ptcn.4 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 ptcn.5 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ Top )
5 ptcn.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
7 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top )
8 toptopon2 ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ Top ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) )
9 7 8 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) )
10 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝑘 ) )
11 6 9 5 10 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝑘 ) )
12 11 fvmptelcdm ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
13 12 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
14 13 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
15 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
16 mptelixpg ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
17 15 16 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
18 14 17 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) )
19 1 ptuni ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ Top ) → X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐾 )
20 3 4 19 syl2anc ⊢ ( 𝜑 → X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐾 )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → X 𝑘 ∈ 𝐼 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐾 )
22 18 21 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ ∪ 𝐾 )
23 22 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) : 𝑋 ⟶ ∪ 𝐾 )
24 2 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
25 3 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
26 4 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐹 : 𝐼 ⟶ Top )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
28 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) )
29 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑧 ∈ 𝑋 )
30 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
31 2 30 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
32 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑋 = ∪ 𝐽 )
33 29 32 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑧 ∈ ∪ 𝐽 )
34 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
35 34 cncnpi ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐽 Cn ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑧 ∈ ∪ 𝐽 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) )
36 28 33 35 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝑧 ) )
37 1 24 25 26 27 36 ptcnp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑧 ) )
38 37 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑧 ) )
39 pttop ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ Top ) → ( ∏t ‘ 𝐹 ) ∈ Top )
40 3 4 39 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ 𝐹 ) ∈ Top )
41 1 40 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ Top )
42 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
43 41 42 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
44 cncnp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) : 𝑋 ⟶ ∪ 𝐾 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑧 ) ) ) )
45 2 43 44 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) : 𝑋 ⟶ ∪ 𝐾 ∧ ∀ 𝑧 ∈ 𝑋 ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑧 ) ) ) )
46 23 38 45 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) )