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