Metamath Proof Explorer

Theorem lmcn2

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 15-May-2014)

Ref Expression
Hypotheses txlm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
txlm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
txlm.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
txlm.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
txlm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
txlm.g ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ 𝑌 )
lmcn2.fl ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑅 )
lmcn2.gl ⊢ ( 𝜑 → 𝐺 ( ⇝𝑡 ‘ 𝐾 ) 𝑆 )
lmcn2.o ⊢ ( 𝜑 → 𝑂 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) )
lmcn2.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) 𝑂 ( 𝐺 ‘ 𝑛 ) ) )
Assertion lmcn2 ( 𝜑 → 𝐻 ( ⇝𝑡 ‘ 𝑁 ) ( 𝑅 𝑂 𝑆 ) )

Proof

Step Hyp Ref Expression
1 txlm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 txlm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 txlm.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 txlm.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
5 txlm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
6 txlm.g ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ 𝑌 )
7 lmcn2.fl ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑅 )
8 lmcn2.gl ⊢ ( 𝜑 → 𝐺 ( ⇝𝑡 ‘ 𝐾 ) 𝑆 )
9 lmcn2.o ⊢ ( 𝜑 → 𝑂 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) )
10 lmcn2.h ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) 𝑂 ( 𝐺 ‘ 𝑛 ) ) )
11 5 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 )
12 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑛 ) ∈ 𝑌 )
13 11 12 opelxpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
14 eqidd ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ) = ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ) )
15 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
16 3 4 15 syl2anc ⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
17 cntop2 ⊢ ( 𝑂 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) → 𝑁 ∈ Top )
18 9 17 syl ⊢ ( 𝜑 → 𝑁 ∈ Top )
19 toptopon2 ⊢ ( 𝑁 ∈ Top ↔ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
20 18 19 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
21 cnf2 ⊢ ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) ∧ 𝑂 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑁 ) ) → 𝑂 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑁 )
22 16 20 9 21 syl3anc ⊢ ( 𝜑 → 𝑂 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑁 )
23 22 feqmptd ⊢ ( 𝜑 → 𝑂 = ( 𝑥 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑂 ‘ 𝑥 ) ) )
24 fveq2 ⊢ ( 𝑥 = ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ) )
25 df-ov ⊢ ( ( 𝐹 ‘ 𝑛 ) 𝑂 ( 𝐺 ‘ 𝑛 ) ) = ( 𝑂 ‘ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ )
26 24 25 eqtr4di ⊢ ( 𝑥 = ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ → ( 𝑂 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) 𝑂 ( 𝐺 ‘ 𝑛 ) ) )
27 13 14 23 26 fmptco ⊢ ( 𝜑 → ( 𝑂 ∘ ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) 𝑂 ( 𝐺 ‘ 𝑛 ) ) ) )
28 27 10 eqtr4di ⊢ ( 𝜑 → ( 𝑂 ∘ ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ) ) = 𝐻 )
29 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ) = ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ )
30 1 2 3 4 5 6 29 txlm ⊢ ( 𝜑 → ( ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑅 ∧ 𝐺 ( ⇝𝑡 ‘ 𝐾 ) 𝑆 ) ↔ ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ) ( ⇝𝑡 ‘ ( 𝐽 ×t 𝐾 ) ) ⟨ 𝑅 , 𝑆 ⟩ ) )
31 7 8 30 mpbi2and ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ) ( ⇝𝑡 ‘ ( 𝐽 ×t 𝐾 ) ) ⟨ 𝑅 , 𝑆 ⟩ )
32 31 9 lmcn ⊢ ( 𝜑 → ( 𝑂 ∘ ( 𝑛 ∈ 𝑍 ↦ ⟨ ( 𝐹 ‘ 𝑛 ) , ( 𝐺 ‘ 𝑛 ) ⟩ ) ) ( ⇝𝑡 ‘ 𝑁 ) ( 𝑂 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) )
33 28 32 eqbrtrrd ⊢ ( 𝜑 → 𝐻 ( ⇝𝑡 ‘ 𝑁 ) ( 𝑂 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) )
34 df-ov ⊢ ( 𝑅 𝑂 𝑆 ) = ( 𝑂 ‘ ⟨ 𝑅 , 𝑆 ⟩ )
35 33 34 breqtrrdi ⊢ ( 𝜑 → 𝐻 ( ⇝𝑡 ‘ 𝑁 ) ( 𝑅 𝑂 𝑆 ) )