Step | Hyp | Ref
| Expression |
1 | | df-ov 6653 |
. . . . . . . . . 10
⊢ (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉) |
2 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋) |
3 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌) |
4 | | cnmpt21.j |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
5 | | cnmpt21.k |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
6 | | txtopon 21394 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
7 | 4, 5, 6 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
8 | | cnmpt21.l |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) |
9 | | cnmpt21.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
10 | | cnf2 21053 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍) |
11 | 7, 8, 9, 10 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍) |
12 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
13 | 12 | fmpt2 7237 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍 ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍) |
14 | 11, 13 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍) |
15 | | rsp2 2936 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑍)) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑍)) |
17 | 16 | imp 445 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝐴 ∈ 𝑍) |
18 | 12 | ovmpt4g 6783 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐴 ∈ 𝑍) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = 𝐴) |
19 | 2, 3, 17, 18 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = 𝐴) |
20 | 1, 19 | syl5eqr 2670 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉) = 𝐴) |
21 | 20 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑧 ∈ 𝑍 ↦ 𝐵)‘((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉)) = ((𝑧 ∈ 𝑍 ↦ 𝐵)‘𝐴)) |
22 | | cnmpt21.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) |
23 | | cntop2 21045 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀) → 𝑀 ∈ Top) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Top) |
25 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑀 =
∪ 𝑀 |
26 | 25 | toptopon 20722 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘∪ 𝑀)) |
27 | 24, 26 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (TopOn‘∪ 𝑀)) |
28 | | cnf2 21053 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘∪ 𝑀)
∧ (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) → (𝑧 ∈ 𝑍 ↦ 𝐵):𝑍⟶∪ 𝑀) |
29 | 8, 27, 22, 28 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵):𝑍⟶∪ 𝑀) |
30 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑍 ↦ 𝐵) = (𝑧 ∈ 𝑍 ↦ 𝐵) |
31 | 30 | fmpt 6381 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑍 𝐵 ∈ ∪ 𝑀 ↔ (𝑧 ∈ 𝑍 ↦ 𝐵):𝑍⟶∪ 𝑀) |
32 | 29, 31 | sylibr 224 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ 𝑍 𝐵 ∈ ∪ 𝑀) |
33 | 32 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ∀𝑧 ∈ 𝑍 𝐵 ∈ ∪ 𝑀) |
34 | | cnmpt21.c |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) |
35 | 34 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → (𝐵 ∈ ∪ 𝑀 ↔ 𝐶 ∈ ∪ 𝑀)) |
36 | 35 | rspcv 3305 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑍 → (∀𝑧 ∈ 𝑍 𝐵 ∈ ∪ 𝑀 → 𝐶 ∈ ∪ 𝑀)) |
37 | 17, 33, 36 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝐶 ∈ ∪ 𝑀) |
38 | 34, 30 | fvmptg 6280 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑍 ∧ 𝐶 ∈ ∪ 𝑀) → ((𝑧 ∈ 𝑍 ↦ 𝐵)‘𝐴) = 𝐶) |
39 | 17, 37, 38 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑧 ∈ 𝑍 ↦ 𝐵)‘𝐴) = 𝐶) |
40 | 21, 39 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑧 ∈ 𝑍 ↦ 𝐵)‘((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉)) = 𝐶) |
41 | | opelxpi 5148 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑌)) |
42 | | fvco3 6275 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍 ∧ 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑌)) → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑧 ∈ 𝑍 ↦ 𝐵)‘((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉))) |
43 | 11, 41, 42 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑧 ∈ 𝑍 ↦ 𝐵)‘((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉))) |
44 | | df-ov 6653 |
. . . . . . . 8
⊢ (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)𝑦) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) |
45 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) |
46 | 45 | ovmpt4g 6783 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐶 ∈ ∪ 𝑀) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)𝑦) = 𝐶) |
47 | 2, 3, 37, 46 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)𝑦) = 𝐶) |
48 | 44, 47 | syl5eqr 2670 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) = 𝐶) |
49 | 40, 43, 48 | 3eqtr4d 2666 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉)) |
50 | 49 | ralrimivva 2971 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉)) |
51 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑢∀𝑦 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) |
52 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥𝑌 |
53 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑧 ∈ 𝑍 ↦ 𝐵) |
54 | | nfmpt21 6722 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
55 | 53, 54 | nfco 5287 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) |
56 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥〈𝑢, 𝑣〉 |
57 | 55, 56 | nffv 6198 |
. . . . . . . 8
⊢
Ⅎ𝑥(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) |
58 | | nfmpt21 6722 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) |
59 | 58, 56 | nffv 6198 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉) |
60 | 57, 59 | nfeq 2776 |
. . . . . . 7
⊢
Ⅎ𝑥(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉) |
61 | 52, 60 | nfral 2945 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉) |
62 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑣(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) |
63 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑧 ∈ 𝑍 ↦ 𝐵) |
64 | | nfmpt22 6723 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
65 | 63, 64 | nfco 5287 |
. . . . . . . . . 10
⊢
Ⅎ𝑦((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) |
66 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑦〈𝑥, 𝑣〉 |
67 | 65, 66 | nffv 6198 |
. . . . . . . . 9
⊢
Ⅎ𝑦(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) |
68 | | nfmpt22 6723 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) |
69 | 68, 66 | nffv 6198 |
. . . . . . . . 9
⊢
Ⅎ𝑦((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) |
70 | 67, 69 | nfeq 2776 |
. . . . . . . 8
⊢
Ⅎ𝑦(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) |
71 | | opeq2 4403 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑣〉) |
72 | 71 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉)) |
73 | 71 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉)) |
74 | 72, 73 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → ((((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) ↔ (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉))) |
75 | 62, 70, 74 | cbvral 3167 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) ↔ ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉)) |
76 | | opeq1 4402 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → 〈𝑥, 𝑣〉 = 〈𝑢, 𝑣〉) |
77 | 76 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉)) |
78 | 76 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
79 | 77, 78 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) ↔ (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉))) |
80 | 79 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) ↔ ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉))) |
81 | 75, 80 | syl5bb 272 |
. . . . . 6
⊢ (𝑥 = 𝑢 → (∀𝑦 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) ↔ ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉))) |
82 | 51, 61, 81 | cbvral 3167 |
. . . . 5
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) ↔ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
83 | 50, 82 | sylib 208 |
. . . 4
⊢ (𝜑 → ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
84 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉)) |
85 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
86 | 84, 85 | eqeq12d 2637 |
. . . . 5
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ((((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤) ↔ (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉))) |
87 | 86 | ralxp 5263 |
. . . 4
⊢
(∀𝑤 ∈
(𝑋 × 𝑌)(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤) ↔ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
88 | 83, 87 | sylibr 224 |
. . 3
⊢ (𝜑 → ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤)) |
89 | | fco 6058 |
. . . . . 6
⊢ (((𝑧 ∈ 𝑍 ↦ 𝐵):𝑍⟶∪ 𝑀 ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)):(𝑋 × 𝑌)⟶∪ 𝑀) |
90 | 29, 11, 89 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)):(𝑋 × 𝑌)⟶∪ 𝑀) |
91 | | ffn 6045 |
. . . . 5
⊢ (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)):(𝑋 × 𝑌)⟶∪ 𝑀 → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) Fn (𝑋 × 𝑌)) |
92 | 90, 91 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) Fn (𝑋 × 𝑌)) |
93 | 37 | ralrimivva 2971 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ ∪ 𝑀) |
94 | 45 | fmpt2 7237 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ ∪ 𝑀 ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶):(𝑋 × 𝑌)⟶∪ 𝑀) |
95 | 93, 94 | sylib 208 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶):(𝑋 × 𝑌)⟶∪ 𝑀) |
96 | | ffn 6045 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶):(𝑋 × 𝑌)⟶∪ 𝑀 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) Fn (𝑋 × 𝑌)) |
97 | 95, 96 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) Fn (𝑋 × 𝑌)) |
98 | | eqfnfv 6311 |
. . . 4
⊢ ((((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) Fn (𝑋 × 𝑌) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) Fn (𝑋 × 𝑌)) → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤))) |
99 | 92, 97, 98 | syl2anc 693 |
. . 3
⊢ (𝜑 → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤))) |
100 | 88, 99 | mpbird 247 |
. 2
⊢ (𝜑 → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)) |
101 | | cnco 21070 |
. . 3
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
102 | 9, 22, 101 | syl2anc 693 |
. 2
⊢ (𝜑 → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
103 | 100, 102 | eqeltrrd 2702 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |