Metamath Proof Explorer

Theorem flfcnp2

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, 19-Sep-2015)

Ref Expression
Hypotheses flfcnp2.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
flfcnp2.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
flfcnp2.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑍 ) )
flfcnp2.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐴 ∈ 𝑋 )
flfcnp2.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ 𝑌 )
flfcnp2.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ) )
flfcnp2.s ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ) )
flfcnp2.o ⊢ ( 𝜑 → 𝑂 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝑁 ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) )
Assertion flfcnp2 ( 𝜑 → ( 𝑅 𝑂 𝑆 ) ∈ ( ( 𝑁 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 𝑂 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 flfcnp2.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 flfcnp2.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 flfcnp2.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑍 ) )
4 flfcnp2.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐴 ∈ 𝑋 )
5 flfcnp2.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ 𝑌 )
6 flfcnp2.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ) )
7 flfcnp2.s ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ) )
8 flfcnp2.o ⊢ ( 𝜑 → 𝑂 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝑁 ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) )
9 df-ov ⊢ ( 𝑅 𝑂 𝑆 ) = ( 𝑂 ‘ ⟨ 𝑅 , 𝑆 ⟩ )
10 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
11 1 2 10 syl2anc ⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
12 4 5 opelxpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) )
13 12 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) : 𝑍 ⟶ ( 𝑋 × 𝑌 ) )
14 4 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) : 𝑍 ⟶ 𝑋 )
15 5 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ 𝑌 )
16 nfcv ⊢ Ⅎ 𝑦 ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) ⟩
17 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑦 )
18 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑦 )
19 17 18 nfop ⊢ Ⅎ 𝑥 ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑦 ) ⟩
20 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑦 ) )
21 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑦 ) )
22 20 21 opeq12d ⊢ ( 𝑥 = 𝑦 → ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑦 ) ⟩ )
23 16 19 22 cbvmpt ⊢ ( 𝑥 ∈ 𝑍 ↦ ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) = ( 𝑦 ∈ 𝑍 ↦ ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑦 ) ⟩ )
24 1 2 3 14 15 23 txflf ⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) ) ↔ ( 𝑅 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ) ∧ 𝑆 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ) ) ) )
25 6 7 24 mpbir2and ⊢ ( 𝜑 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) ) )
26 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝑥 ∈ 𝑍 )
27 eqid ⊢ ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑍 ↦ 𝐴 )
28 27 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
29 26 4 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
30 eqid ⊢ ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑍 ↦ 𝐵 )
31 30 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑍 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
32 26 5 31 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
33 29 32 opeq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
34 33 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
35 34 fveq2d ⊢ ( 𝜑 → ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ⟨ ( ( 𝑥 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑥 ) ⟩ ) ) = ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
36 25 35 eleqtrd ⊢ ( 𝜑 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
37 flfcnp ⊢ ( ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( Fil ‘ 𝑍 ) ∧ ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) : 𝑍 ⟶ ( 𝑋 × 𝑌 ) ) ∧ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( ( 𝐽 ×t 𝐾 ) fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∧ 𝑂 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝑁 ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ) → ( 𝑂 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ∈ ( ( 𝑁 fLimf 𝐿 ) ‘ ( 𝑂 ∘ ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
38 11 3 13 36 8 37 syl32anc ⊢ ( 𝜑 → ( 𝑂 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ∈ ( ( 𝑁 fLimf 𝐿 ) ‘ ( 𝑂 ∘ ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
39 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
40 cnptop2 ⊢ ( 𝑂 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝑁 ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) → 𝑁 ∈ Top )
41 8 40 syl ⊢ ( 𝜑 → 𝑁 ∈ Top )
42 toptopon2 ⊢ ( 𝑁 ∈ Top ↔ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
43 41 42 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) )
44 cnpf2 ⊢ ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝑁 ∈ ( TopOn ‘ ∪ 𝑁 ) ∧ 𝑂 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝑁 ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) → 𝑂 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑁 )
45 11 43 8 44 syl3anc ⊢ ( 𝜑 → 𝑂 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑁 )
46 45 feqmptd ⊢ ( 𝜑 → 𝑂 = ( 𝑦 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑂 ‘ 𝑦 ) ) )
47 fveq2 ⊢ ( 𝑦 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑂 ‘ 𝑦 ) = ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
48 df-ov ⊢ ( 𝐴 𝑂 𝐵 ) = ( 𝑂 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
49 47 48 eqtr4di ⊢ ( 𝑦 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑂 ‘ 𝑦 ) = ( 𝐴 𝑂 𝐵 ) )
50 12 39 46 49 fmptco ⊢ ( 𝜑 → ( 𝑂 ∘ ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 𝑂 𝐵 ) ) )
51 50 fveq2d ⊢ ( 𝜑 → ( ( 𝑁 fLimf 𝐿 ) ‘ ( 𝑂 ∘ ( 𝑥 ∈ 𝑍 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ) ) = ( ( 𝑁 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 𝑂 𝐵 ) ) ) )
52 38 51 eleqtrd ⊢ ( 𝜑 → ( 𝑂 ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ∈ ( ( 𝑁 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 𝑂 𝐵 ) ) ) )
53 9 52 eqeltrid ⊢ ( 𝜑 → ( 𝑅 𝑂 𝑆 ) ∈ ( ( 𝑁 fLimf 𝐿 ) ‘ ( 𝑥 ∈ 𝑍 ↦ ( 𝐴 𝑂 𝐵 ) ) ) )