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

Metamath Proof Explorer

Theorem cnmpt2t

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmpt21.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
cnmpt21.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
cnmpt21.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
cnmpt2t.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )
Assertion cnmpt2t ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( 𝐿 ×t 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 cnmpt21.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmpt21.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 cnmpt21.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
4 cnmpt2t.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )
5 fveq2 ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
6 df-ov ⊢ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
7 5 6 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) = ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) )
8 fveq2 ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
9 df-ov ⊢ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
10 8 9 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) = ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) )
11 7 10 opeq12d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ = ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩ )
12 11 mpompt ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑢 ∈ 𝑋 , 𝑣 ∈ 𝑌 ↦ ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩ )
13 nfcv ⊢ Ⅎ 𝑥 𝑢
14 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
15 nfcv ⊢ Ⅎ 𝑥 𝑣
16 13 14 15 nfov ⊢ Ⅎ 𝑥 ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 )
17 nfmpo1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
18 13 17 15 nfov ⊢ Ⅎ 𝑥 ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 )
19 16 18 nfop ⊢ Ⅎ 𝑥 ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩
20 nfcv ⊢ Ⅎ 𝑦 𝑢
21 nfmpo2 ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
22 nfcv ⊢ Ⅎ 𝑦 𝑣
23 20 21 22 nfov ⊢ Ⅎ 𝑦 ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 )
24 nfmpo2 ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
25 20 24 22 nfov ⊢ Ⅎ 𝑦 ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 )
26 23 25 nfop ⊢ Ⅎ 𝑦 ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩
27 nfcv ⊢ Ⅎ 𝑢 ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩
28 nfcv ⊢ Ⅎ 𝑣 ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩
29 oveq12 ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) = ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) )
30 oveq12 ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) = ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) )
31 29 30 opeq12d ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩ = ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ )
32 19 26 27 28 31 cbvmpo ⊢ ( 𝑢 ∈ 𝑋 , 𝑣 ∈ 𝑌 ↦ ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ )
33 12 32 eqtri ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ )
34 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
35 1 2 34 syl2anc ⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
36 toponuni ⊢ ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝐽 ×t 𝐾 ) )
37 mpteq1 ⊢ ( ( 𝑋 × 𝑌 ) = ∪ ( 𝐽 ×t 𝐾 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑧 ∈ ∪ ( 𝐽 ×t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) )
38 35 36 37 3syl ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑧 ∈ ∪ ( 𝐽 ×t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) )
39 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
40 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
41 cntop2 ⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) → 𝐿 ∈ Top )
42 3 41 syl ⊢ ( 𝜑 → 𝐿 ∈ Top )
43 toptopon2 ⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
44 42 43 sylib ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
45 cnf2 ⊢ ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
46 35 44 3 45 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
47 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
48 47 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
49 46 48 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 )
50 rsp2 ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ∪ 𝐿 ) )
51 49 50 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ∪ 𝐿 ) )
52 51 3impib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ∪ 𝐿 )
53 47 ovmpt4g ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐴 ∈ ∪ 𝐿 ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) = 𝐴 )
54 39 40 52 53 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) = 𝐴 )
55 cntop2 ⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) → 𝑀 ∈ Top )
56 4 55 syl ⊢ ( 𝜑 → 𝑀 ∈ Top )
57 toptopon2 ⊢ ( 𝑀 ∈ Top ↔ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
58 56 57 sylib ⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
59 cnf2 ⊢ ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑀 )
60 35 58 4 59 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑀 )
61 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
62 61 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑀 )
63 60 62 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 )
64 rsp2 ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ∪ 𝑀 ) )
65 63 64 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ∪ 𝑀 ) )
66 65 3impib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ∪ 𝑀 )
67 61 ovmpt4g ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐵 ∈ ∪ 𝑀 ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) = 𝐵 )
68 39 40 66 67 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) = 𝐵 )
69 54 68 opeq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
70 69 mpoeq3dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
71 33 38 70 3eqtr3a ⊢ ( 𝜑 → ( 𝑧 ∈ ∪ ( 𝐽 ×t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
72 eqid ⊢ ∪ ( 𝐽 ×t 𝐾 ) = ∪ ( 𝐽 ×t 𝐾 )
73 eqid ⊢ ( 𝑧 ∈ ∪ ( 𝐽 ×t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑧 ∈ ∪ ( 𝐽 ×t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ )
74 72 73 txcnmpt ⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) ) → ( 𝑧 ∈ ∪ ( 𝐽 ×t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( 𝐿 ×t 𝑀 ) ) )
75 3 4 74 syl2anc ⊢ ( 𝜑 → ( 𝑧 ∈ ∪ ( 𝐽 ×t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( 𝐿 ×t 𝑀 ) ) )
76 71 75 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn ( 𝐿 ×t 𝑀 ) ) )