| Step | Hyp | Ref
| Expression |
| 1 | | df-ov 7434 |
. . . . . . . . . 10
⊢ (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉) |
| 2 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑥 ∈ 𝑋) |
| 3 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝑦 ∈ 𝑌) |
| 4 | | cnmpt21.j |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 5 | | cnmpt21.k |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
| 6 | | txtopon 23599 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
| 7 | 4, 5, 6 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
| 8 | | cnmpt21.l |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) |
| 9 | | cnmpt21.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
| 10 | | cnf2 23257 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍) |
| 11 | 7, 8, 9, 10 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍) |
| 12 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
| 13 | 12 | fmpo 8093 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍 ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍) |
| 14 | 11, 13 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍) |
| 15 | | rsp2 3277 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑍)) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑍)) |
| 17 | 16 | imp 406 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝐴 ∈ 𝑍) |
| 18 | 12 | ovmpt4g 7580 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐴 ∈ 𝑍) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = 𝐴) |
| 19 | 2, 3, 17, 18 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = 𝐴) |
| 20 | 1, 19 | eqtr3id 2791 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉) = 𝐴) |
| 21 | 20 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑧 ∈ 𝑍 ↦ 𝐵)‘((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉)) = ((𝑧 ∈ 𝑍 ↦ 𝐵)‘𝐴)) |
| 22 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑍 ↦ 𝐵) = (𝑧 ∈ 𝑍 ↦ 𝐵) |
| 23 | | cnmpt21.c |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) |
| 24 | 23 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → (𝐵 ∈ ∪ 𝑀 ↔ 𝐶 ∈ ∪ 𝑀)) |
| 25 | | cnmpt21.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) |
| 26 | | cntop2 23249 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀) → 𝑀 ∈ Top) |
| 27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Top) |
| 28 | | toptopon2 22924 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘∪ 𝑀)) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (TopOn‘∪ 𝑀)) |
| 30 | | cnf2 23257 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘∪ 𝑀)
∧ (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) → (𝑧 ∈ 𝑍 ↦ 𝐵):𝑍⟶∪ 𝑀) |
| 31 | 8, 29, 25, 30 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵):𝑍⟶∪ 𝑀) |
| 32 | 22 | fmpt 7130 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑍 𝐵 ∈ ∪ 𝑀 ↔ (𝑧 ∈ 𝑍 ↦ 𝐵):𝑍⟶∪ 𝑀) |
| 33 | 31, 32 | sylibr 234 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ 𝑍 𝐵 ∈ ∪ 𝑀) |
| 34 | 33 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ∀𝑧 ∈ 𝑍 𝐵 ∈ ∪ 𝑀) |
| 35 | 24, 34, 17 | rspcdva 3623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → 𝐶 ∈ ∪ 𝑀) |
| 36 | 22, 23, 17, 35 | fvmptd3 7039 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑧 ∈ 𝑍 ↦ 𝐵)‘𝐴) = 𝐶) |
| 37 | 21, 36 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑧 ∈ 𝑍 ↦ 𝐵)‘((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉)) = 𝐶) |
| 38 | | opelxpi 5722 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑌)) |
| 39 | | fvco3 7008 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍 ∧ 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑌)) → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑧 ∈ 𝑍 ↦ 𝐵)‘((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉))) |
| 40 | 11, 38, 39 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑧 ∈ 𝑍 ↦ 𝐵)‘((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑥, 𝑦〉))) |
| 41 | | df-ov 7434 |
. . . . . . . 8
⊢ (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)𝑦) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) |
| 42 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) |
| 43 | 42 | ovmpt4g 7580 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐶 ∈ ∪ 𝑀) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)𝑦) = 𝐶) |
| 44 | 2, 3, 35, 43 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)𝑦) = 𝐶) |
| 45 | 41, 44 | eqtr3id 2791 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) = 𝐶) |
| 46 | 37, 40, 45 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉)) |
| 47 | 46 | ralrimivva 3202 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉)) |
| 48 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑢∀𝑦 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) |
| 49 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑥𝑌 |
| 50 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑧 ∈ 𝑍 ↦ 𝐵) |
| 51 | | nfmpo1 7513 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
| 52 | 50, 51 | nfco 5876 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) |
| 53 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥〈𝑢, 𝑣〉 |
| 54 | 52, 53 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑥(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) |
| 55 | | nfmpo1 7513 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) |
| 56 | 55, 53 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉) |
| 57 | 54, 56 | nfeq 2919 |
. . . . . . 7
⊢
Ⅎ𝑥(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉) |
| 58 | 49, 57 | nfralw 3311 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉) |
| 59 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑣(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) |
| 60 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑧 ∈ 𝑍 ↦ 𝐵) |
| 61 | | nfmpo2 7514 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
| 62 | 60, 61 | nfco 5876 |
. . . . . . . . . 10
⊢
Ⅎ𝑦((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) |
| 63 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑦〈𝑥, 𝑣〉 |
| 64 | 62, 63 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑦(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) |
| 65 | | nfmpo2 7514 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) |
| 66 | 65, 63 | nffv 6916 |
. . . . . . . . 9
⊢
Ⅎ𝑦((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) |
| 67 | 64, 66 | nfeq 2919 |
. . . . . . . 8
⊢
Ⅎ𝑦(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) |
| 68 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑣〉) |
| 69 | 68 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉)) |
| 70 | 68 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉)) |
| 71 | 69, 70 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → ((((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) ↔ (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉))) |
| 72 | 59, 67, 71 | cbvralw 3306 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) ↔ ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉)) |
| 73 | | opeq1 4873 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → 〈𝑥, 𝑣〉 = 〈𝑢, 𝑣〉) |
| 74 | 73 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉)) |
| 75 | 73 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
| 76 | 74, 75 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) ↔ (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉))) |
| 77 | 76 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑣〉) ↔ ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉))) |
| 78 | 72, 77 | bitrid 283 |
. . . . . 6
⊢ (𝑥 = 𝑢 → (∀𝑦 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) ↔ ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉))) |
| 79 | 48, 58, 78 | cbvralw 3306 |
. . . . 5
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑥, 𝑦〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑥, 𝑦〉) ↔ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
| 80 | 47, 79 | sylib 218 |
. . . 4
⊢ (𝜑 → ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
| 81 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉)) |
| 82 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
| 83 | 81, 82 | eqeq12d 2753 |
. . . . 5
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ((((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤) ↔ (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉))) |
| 84 | 83 | ralxp 5852 |
. . . 4
⊢
(∀𝑤 ∈
(𝑋 × 𝑌)(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤) ↔ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘〈𝑢, 𝑣〉) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘〈𝑢, 𝑣〉)) |
| 85 | 80, 84 | sylibr 234 |
. . 3
⊢ (𝜑 → ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤)) |
| 86 | | fco 6760 |
. . . . . 6
⊢ (((𝑧 ∈ 𝑍 ↦ 𝐵):𝑍⟶∪ 𝑀 ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶𝑍) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)):(𝑋 × 𝑌)⟶∪ 𝑀) |
| 87 | 31, 11, 86 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)):(𝑋 × 𝑌)⟶∪ 𝑀) |
| 88 | 87 | ffnd 6737 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) Fn (𝑋 × 𝑌)) |
| 89 | 35 | ralrimivva 3202 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ ∪ 𝑀) |
| 90 | 42 | fmpo 8093 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ ∪ 𝑀 ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶):(𝑋 × 𝑌)⟶∪ 𝑀) |
| 91 | 89, 90 | sylib 218 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶):(𝑋 × 𝑌)⟶∪ 𝑀) |
| 92 | 91 | ffnd 6737 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) Fn (𝑋 × 𝑌)) |
| 93 | | eqfnfv 7051 |
. . . 4
⊢ ((((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) Fn (𝑋 × 𝑌) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) Fn (𝑋 × 𝑌)) → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤))) |
| 94 | 88, 92, 93 | syl2anc 584 |
. . 3
⊢ (𝜑 → (((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ↔ ∀𝑤 ∈ (𝑋 × 𝑌)(((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)‘𝑤))) |
| 95 | 85, 94 | mpbird 257 |
. 2
⊢ (𝜑 → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶)) |
| 96 | | cnco 23274 |
. . 3
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
| 97 | 9, 25, 96 | syl2anc 584 |
. 2
⊢ (𝜑 → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
| 98 | 95, 97 | eqeltrrd 2842 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |