Metamath Proof Explorer


Theorem cnmpt21

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 𝐿 ) )
cnmpt21.l ( 𝜑𝐿 ∈ ( TopOn ‘ 𝑍 ) )
cnmpt21.b ( 𝜑 → ( 𝑧𝑍𝐵 ) ∈ ( 𝐿 Cn 𝑀 ) )
cnmpt21.c ( 𝑧 = 𝐴𝐵 = 𝐶 )
Assertion cnmpt21 ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )

Proof

Step Hyp Ref Expression
1 cnmpt21.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmpt21.k ( 𝜑𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 cnmpt21.a ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
4 cnmpt21.l ( 𝜑𝐿 ∈ ( TopOn ‘ 𝑍 ) )
5 cnmpt21.b ( 𝜑 → ( 𝑧𝑍𝐵 ) ∈ ( 𝐿 Cn 𝑀 ) )
6 cnmpt21.c ( 𝑧 = 𝐴𝐵 = 𝐶 )
7 df-ov ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
8 simprl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → 𝑥𝑋 )
9 simprr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → 𝑦𝑌 )
10 txtopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
11 1 2 10 syl2anc ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
12 cnf2 ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ) → ( 𝑥𝑋 , 𝑦𝑌𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 )
13 11 4 3 12 syl3anc ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 )
14 eqid ( 𝑥𝑋 , 𝑦𝑌𝐴 ) = ( 𝑥𝑋 , 𝑦𝑌𝐴 )
15 14 fmpo ( ∀ 𝑥𝑋𝑦𝑌 𝐴𝑍 ↔ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 )
16 13 15 sylibr ( 𝜑 → ∀ 𝑥𝑋𝑦𝑌 𝐴𝑍 )
17 rsp2 ( ∀ 𝑥𝑋𝑦𝑌 𝐴𝑍 → ( ( 𝑥𝑋𝑦𝑌 ) → 𝐴𝑍 ) )
18 16 17 syl ( 𝜑 → ( ( 𝑥𝑋𝑦𝑌 ) → 𝐴𝑍 ) )
19 18 imp ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → 𝐴𝑍 )
20 14 ovmpt4g ( ( 𝑥𝑋𝑦𝑌𝐴𝑍 ) → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = 𝐴 )
21 8 9 19 20 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 ) 𝑦 ) = 𝐴 )
22 7 21 eqtr3id ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐴 )
23 22 fveq2d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ( ( 𝑧𝑍𝐵 ) ‘ ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = ( ( 𝑧𝑍𝐵 ) ‘ 𝐴 ) )
24 eqid ( 𝑧𝑍𝐵 ) = ( 𝑧𝑍𝐵 )
25 6 eleq1d ( 𝑧 = 𝐴 → ( 𝐵 𝑀𝐶 𝑀 ) )
26 cntop2 ( ( 𝑧𝑍𝐵 ) ∈ ( 𝐿 Cn 𝑀 ) → 𝑀 ∈ Top )
27 5 26 syl ( 𝜑𝑀 ∈ Top )
28 toptopon2 ( 𝑀 ∈ Top ↔ 𝑀 ∈ ( TopOn ‘ 𝑀 ) )
29 27 28 sylib ( 𝜑𝑀 ∈ ( TopOn ‘ 𝑀 ) )
30 cnf2 ( ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ 𝑀 ∈ ( TopOn ‘ 𝑀 ) ∧ ( 𝑧𝑍𝐵 ) ∈ ( 𝐿 Cn 𝑀 ) ) → ( 𝑧𝑍𝐵 ) : 𝑍 𝑀 )
31 4 29 5 30 syl3anc ( 𝜑 → ( 𝑧𝑍𝐵 ) : 𝑍 𝑀 )
32 24 fmpt ( ∀ 𝑧𝑍 𝐵 𝑀 ↔ ( 𝑧𝑍𝐵 ) : 𝑍 𝑀 )
33 31 32 sylibr ( 𝜑 → ∀ 𝑧𝑍 𝐵 𝑀 )
34 33 adantr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ∀ 𝑧𝑍 𝐵 𝑀 )
35 25 34 19 rspcdva ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → 𝐶 𝑀 )
36 24 6 19 35 fvmptd3 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ( ( 𝑧𝑍𝐵 ) ‘ 𝐴 ) = 𝐶 )
37 23 36 eqtrd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ( ( 𝑧𝑍𝐵 ) ‘ ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) = 𝐶 )
38 opelxpi ( ( 𝑥𝑋𝑦𝑌 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) )
39 fvco3 ( ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑧𝑍𝐵 ) ‘ ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
40 13 38 39 syl2an ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑧𝑍𝐵 ) ‘ ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
41 df-ov ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐶 ) 𝑦 ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
42 eqid ( 𝑥𝑋 , 𝑦𝑌𝐶 ) = ( 𝑥𝑋 , 𝑦𝑌𝐶 )
43 42 ovmpt4g ( ( 𝑥𝑋𝑦𝑌𝐶 𝑀 ) → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐶 ) 𝑦 ) = 𝐶 )
44 8 9 35 43 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ( 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐶 ) 𝑦 ) = 𝐶 )
45 41 44 eqtr3id ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐶 )
46 37 40 45 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑌 ) ) → ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
47 46 ralrimivva ( 𝜑 → ∀ 𝑥𝑋𝑦𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
48 nfv 𝑢𝑦𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
49 nfcv 𝑥 𝑌
50 nfcv 𝑥 ( 𝑧𝑍𝐵 )
51 nfmpo1 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐴 )
52 50 51 nfco 𝑥 ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) )
53 nfcv 𝑥𝑢 , 𝑣
54 52 53 nffv 𝑥 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
55 nfmpo1 𝑥 ( 𝑥𝑋 , 𝑦𝑌𝐶 )
56 55 53 nffv 𝑥 ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
57 54 56 nfeq 𝑥 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
58 49 57 nfralw 𝑥𝑣𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
59 nfv 𝑣 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
60 nfcv 𝑦 ( 𝑧𝑍𝐵 )
61 nfmpo2 𝑦 ( 𝑥𝑋 , 𝑦𝑌𝐴 )
62 60 61 nfco 𝑦 ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) )
63 nfcv 𝑦𝑥 , 𝑣
64 62 63 nffv 𝑦 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑣 ⟩ )
65 nfmpo2 𝑦 ( 𝑥𝑋 , 𝑦𝑌𝐶 )
66 65 63 nffv 𝑦 ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑣 ⟩ )
67 64 66 nfeq 𝑦 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑣 ⟩ )
68 opeq2 ( 𝑦 = 𝑣 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑣 ⟩ )
69 68 fveq2d ( 𝑦 = 𝑣 → ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) )
70 68 fveq2d ( 𝑦 = 𝑣 → ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) )
71 69 70 eqeq12d ( 𝑦 = 𝑣 → ( ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) ) )
72 59 67 71 cbvralw ( ∀ 𝑦𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑣𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) )
73 opeq1 ( 𝑥 = 𝑢 → ⟨ 𝑥 , 𝑣 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ )
74 73 fveq2d ( 𝑥 = 𝑢 → ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) = ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
75 73 fveq2d ( 𝑥 = 𝑢 → ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
76 74 75 eqeq12d ( 𝑥 = 𝑢 → ( ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) ↔ ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ) )
77 76 ralbidv ( 𝑥 = 𝑢 → ( ∀ 𝑣𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑣 ⟩ ) ↔ ∀ 𝑣𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ) )
78 72 77 syl5bb ( 𝑥 = 𝑢 → ( ∀ 𝑦𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑣𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ) )
79 48 58 78 cbvralw ( ∀ 𝑥𝑋𝑦𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑢𝑋𝑣𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
80 47 79 sylib ( 𝜑 → ∀ 𝑢𝑋𝑣𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
81 fveq2 ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ 𝑤 ) = ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
82 fveq2 ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ 𝑤 ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
83 81 82 eqeq12d ( 𝑤 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ 𝑤 ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ 𝑤 ) ↔ ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ) )
84 83 ralxp ( ∀ 𝑤 ∈ ( 𝑋 × 𝑌 ) ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ 𝑤 ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ 𝑤 ) ↔ ∀ 𝑢𝑋𝑣𝑌 ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
85 80 84 sylibr ( 𝜑 → ∀ 𝑤 ∈ ( 𝑋 × 𝑌 ) ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ 𝑤 ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ 𝑤 ) )
86 fco ( ( ( 𝑧𝑍𝐵 ) : 𝑍 𝑀 ∧ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) → ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑀 )
87 31 13 86 syl2anc ( 𝜑 → ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑀 )
88 87 ffnd ( 𝜑 → ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) Fn ( 𝑋 × 𝑌 ) )
89 35 ralrimivva ( 𝜑 → ∀ 𝑥𝑋𝑦𝑌 𝐶 𝑀 )
90 42 fmpo ( ∀ 𝑥𝑋𝑦𝑌 𝐶 𝑀 ↔ ( 𝑥𝑋 , 𝑦𝑌𝐶 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑀 )
91 89 90 sylib ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌𝐶 ) : ( 𝑋 × 𝑌 ) ⟶ 𝑀 )
92 91 ffnd ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌𝐶 ) Fn ( 𝑋 × 𝑌 ) )
93 eqfnfv ( ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) Fn ( 𝑋 × 𝑌 ) ∧ ( 𝑥𝑋 , 𝑦𝑌𝐶 ) Fn ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) = ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ↔ ∀ 𝑤 ∈ ( 𝑋 × 𝑌 ) ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ 𝑤 ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ 𝑤 ) ) )
94 88 92 93 syl2anc ( 𝜑 → ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) = ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ↔ ∀ 𝑤 ∈ ( 𝑋 × 𝑌 ) ( ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ‘ 𝑤 ) = ( ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ‘ 𝑤 ) ) )
95 85 94 mpbird ( 𝜑 → ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) = ( 𝑥𝑋 , 𝑦𝑌𝐶 ) )
96 cnco ( ( ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ∧ ( 𝑧𝑍𝐵 ) ∈ ( 𝐿 Cn 𝑀 ) ) → ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )
97 3 5 96 syl2anc ( 𝜑 → ( ( 𝑧𝑍𝐵 ) ∘ ( 𝑥𝑋 , 𝑦𝑌𝐴 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )
98 95 97 eqeltrrd ( 𝜑 → ( 𝑥𝑋 , 𝑦𝑌𝐶 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝑀 ) )