Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑢, 𝑣〉)) |
2 | | df-ov 6653 |
. . . . . . 7
⊢ (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑢, 𝑣〉) |
3 | 1, 2 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧) = (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣)) |
4 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘〈𝑢, 𝑣〉)) |
5 | | df-ov 6653 |
. . . . . . 7
⊢ (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘〈𝑢, 𝑣〉) |
6 | 4, 5 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧) = (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)) |
7 | 3, 6 | opeq12d 4410 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉 = 〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉) |
8 | 7 | mpt2mpt 6752 |
. . . 4
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑢 ∈ 𝑋, 𝑣 ∈ 𝑌 ↦ 〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉) |
9 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥𝑢 |
10 | | nfmpt21 6722 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
11 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥𝑣 |
12 | 9, 10, 11 | nfov 6676 |
. . . . . 6
⊢
Ⅎ𝑥(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣) |
13 | | nfmpt21 6722 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) |
14 | 9, 13, 11 | nfov 6676 |
. . . . . 6
⊢
Ⅎ𝑥(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣) |
15 | 12, 14 | nfop 4418 |
. . . . 5
⊢
Ⅎ𝑥〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉 |
16 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑦𝑢 |
17 | | nfmpt22 6723 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
18 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑦𝑣 |
19 | 16, 17, 18 | nfov 6676 |
. . . . . 6
⊢
Ⅎ𝑦(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣) |
20 | | nfmpt22 6723 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) |
21 | 16, 20, 18 | nfov 6676 |
. . . . . 6
⊢
Ⅎ𝑦(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣) |
22 | 19, 21 | nfop 4418 |
. . . . 5
⊢
Ⅎ𝑦〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉 |
23 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑢〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉 |
24 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑣〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉 |
25 | | oveq12 6659 |
. . . . . 6
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦)) |
26 | | oveq12 6659 |
. . . . . 6
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)) |
27 | 25, 26 | opeq12d 4410 |
. . . . 5
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = 𝑦) → 〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉 = 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉) |
28 | 15, 22, 23, 24, 27 | cbvmpt2 6734 |
. . . 4
⊢ (𝑢 ∈ 𝑋, 𝑣 ∈ 𝑌 ↦ 〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉) |
29 | 8, 28 | eqtri 2644 |
. . 3
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉) |
30 | | cnmpt21.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
31 | | cnmpt21.k |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
32 | | txtopon 21394 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
33 | 30, 31, 32 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
34 | | toponuni 20719 |
. . . 4
⊢ ((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾)) |
35 | | mpteq1 4737 |
. . . 4
⊢ ((𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾) → (𝑧 ∈ (𝑋 × 𝑌) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉)) |
36 | 33, 34, 35 | 3syl 18 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉)) |
37 | | simp2 1062 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑥 ∈ 𝑋) |
38 | | simp3 1063 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
39 | | cnmpt21.a |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
40 | | cntop2 21045 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) → 𝐿 ∈ Top) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ Top) |
42 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ∪ 𝐿 =
∪ 𝐿 |
43 | 42 | toptopon 20722 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
44 | 41, 43 | sylib 208 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
45 | | cnf2 21053 |
. . . . . . . . . 10
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶∪ 𝐿) |
46 | 33, 44, 39, 45 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶∪ 𝐿) |
47 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
48 | 47 | fmpt2 7237 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶∪ 𝐿) |
49 | 46, 48 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿) |
50 | | rsp2 2936 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ ∪ 𝐿)) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ ∪ 𝐿)) |
52 | 51 | 3impib 1262 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ ∪ 𝐿) |
53 | 47 | ovmpt4g 6783 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐴 ∈ ∪ 𝐿) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = 𝐴) |
54 | 37, 38, 52, 53 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = 𝐴) |
55 | | cnmpt2t.b |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
56 | | cntop2 21045 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀) → 𝑀 ∈ Top) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Top) |
58 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ∪ 𝑀 =
∪ 𝑀 |
59 | 58 | toptopon 20722 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘∪ 𝑀)) |
60 | 57, 59 | sylib 208 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (TopOn‘∪ 𝑀)) |
61 | | cnf2 21053 |
. . . . . . . . . 10
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝑀 ∈ (TopOn‘∪ 𝑀)
∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶∪ 𝑀) |
62 | 33, 60, 55, 61 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶∪ 𝑀) |
63 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) |
64 | 63 | fmpt2 7237 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶∪ 𝑀) |
65 | 62, 64 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀) |
66 | | rsp2 2936 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐵 ∈ ∪ 𝑀)) |
67 | 65, 66 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐵 ∈ ∪ 𝑀)) |
68 | 67 | 3impib 1262 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐵 ∈ ∪ 𝑀) |
69 | 63 | ovmpt4g 6783 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐵 ∈ ∪ 𝑀) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦) = 𝐵) |
70 | 37, 38, 68, 69 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦) = 𝐵) |
71 | 54, 70 | opeq12d 4410 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉 = 〈𝐴, 𝐵〉) |
72 | 71 | mpt2eq3dva 6719 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝐴, 𝐵〉)) |
73 | 29, 36, 72 | 3eqtr3a 2680 |
. 2
⊢ (𝜑 → (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝐴, 𝐵〉)) |
74 | | eqid 2622 |
. . . 4
⊢ ∪ (𝐽
×t 𝐾) =
∪ (𝐽 ×t 𝐾) |
75 | | eqid 2622 |
. . . 4
⊢ (𝑧 ∈ ∪ (𝐽
×t 𝐾)
↦ 〈((𝑥 ∈
𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) |
76 | 74, 75 | txcnmpt 21427 |
. . 3
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) → (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) |
77 | 39, 55, 76 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) |
78 | 73, 77 | eqeltrrd 2702 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝐴, 𝐵〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) |