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 bitrid ⊢ ( 𝑥 = 𝑢 → ( ∀ 𝑦 ∈ 𝑌 ( ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑧 ∈ 𝑍 ↦ 𝐵 ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ) )
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 𝑀 ) )