Step | Hyp | Ref
| Expression |
1 | | fveq2 6437 |
. . . . . . 7
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑢, 𝑣〉)) |
2 | | df-ov 6913 |
. . . . . . 7
⊢ (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘〈𝑢, 𝑣〉) |
3 | 1, 2 | syl6eqr 2879 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧) = (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣)) |
4 | | fveq2 6437 |
. . . . . . 7
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘〈𝑢, 𝑣〉)) |
5 | | df-ov 6913 |
. . . . . . 7
⊢ (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘〈𝑢, 𝑣〉) |
6 | 4, 5 | syl6eqr 2879 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧) = (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)) |
7 | 3, 6 | opeq12d 4633 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉 = 〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉) |
8 | 7 | mpt2mpt 7017 |
. . . 4
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑢 ∈ 𝑋, 𝑣 ∈ 𝑌 ↦ 〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉) |
9 | | nfcv 2969 |
. . . . . . 7
⊢
Ⅎ𝑥𝑢 |
10 | | nfmpt21 6987 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
11 | | nfcv 2969 |
. . . . . . 7
⊢
Ⅎ𝑥𝑣 |
12 | 9, 10, 11 | nfov 6940 |
. . . . . 6
⊢
Ⅎ𝑥(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣) |
13 | | nfmpt21 6987 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) |
14 | 9, 13, 11 | nfov 6940 |
. . . . . 6
⊢
Ⅎ𝑥(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣) |
15 | 12, 14 | nfop 4641 |
. . . . 5
⊢
Ⅎ𝑥〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉 |
16 | | nfcv 2969 |
. . . . . . 7
⊢
Ⅎ𝑦𝑢 |
17 | | nfmpt22 6988 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
18 | | nfcv 2969 |
. . . . . . 7
⊢
Ⅎ𝑦𝑣 |
19 | 16, 17, 18 | nfov 6940 |
. . . . . 6
⊢
Ⅎ𝑦(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣) |
20 | | nfmpt22 6988 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) |
21 | 16, 20, 18 | nfov 6940 |
. . . . . 6
⊢
Ⅎ𝑦(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣) |
22 | 19, 21 | nfop 4641 |
. . . . 5
⊢
Ⅎ𝑦〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉 |
23 | | nfcv 2969 |
. . . . 5
⊢
Ⅎ𝑢〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉 |
24 | | nfcv 2969 |
. . . . 5
⊢
Ⅎ𝑣〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉 |
25 | | oveq12 6919 |
. . . . . 6
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦)) |
26 | | oveq12 6919 |
. . . . . 6
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣) = (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)) |
27 | 25, 26 | opeq12d 4633 |
. . . . 5
⊢ ((𝑢 = 𝑥 ∧ 𝑣 = 𝑦) → 〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉 = 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉) |
28 | 15, 22, 23, 24, 27 | cbvmpt2 6999 |
. . . 4
⊢ (𝑢 ∈ 𝑋, 𝑣 ∈ 𝑌 ↦ 〈(𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑣), (𝑢(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑣)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉) |
29 | 8, 28 | eqtri 2849 |
. . 3
⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉) |
30 | | cnmpt21.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
31 | | cnmpt21.k |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
32 | | txtopon 21772 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
33 | 30, 31, 32 | syl2anc 579 |
. . . 4
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
34 | | toponuni 21096 |
. . . 4
⊢ ((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾)) |
35 | | mpteq1 4962 |
. . . 4
⊢ ((𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾) → (𝑧 ∈ (𝑋 × 𝑌) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉)) |
36 | 33, 34, 35 | 3syl 18 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉)) |
37 | | simp2 1171 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑥 ∈ 𝑋) |
38 | | simp3 1172 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
39 | | cnmpt21.a |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
40 | | cntop2 21423 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) → 𝐿 ∈ Top) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ Top) |
42 | | eqid 2825 |
. . . . . . . . . . . 12
⊢ ∪ 𝐿 =
∪ 𝐿 |
43 | 42 | toptopon 21099 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
44 | 41, 43 | sylib 210 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
45 | | cnf2 21431 |
. . . . . . . . . 10
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶∪ 𝐿) |
46 | 33, 44, 39, 45 | syl3anc 1494 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶∪ 𝐿) |
47 | | eqid 2825 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
48 | 47 | fmpt2 7505 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶∪ 𝐿) |
49 | 46, 48 | sylibr 226 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿) |
50 | | rsp2 3145 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ ∪ 𝐿)) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ ∪ 𝐿)) |
52 | 51 | 3impib 1148 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ ∪ 𝐿) |
53 | 47 | ovmpt4g 7048 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐴 ∈ ∪ 𝐿) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = 𝐴) |
54 | 37, 38, 52, 53 | syl3anc 1494 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦) = 𝐴) |
55 | | cnmpt2t.b |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) |
56 | | cntop2 21423 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀) → 𝑀 ∈ Top) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Top) |
58 | | eqid 2825 |
. . . . . . . . . . . 12
⊢ ∪ 𝑀 =
∪ 𝑀 |
59 | 58 | toptopon 21099 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘∪ 𝑀)) |
60 | 57, 59 | sylib 210 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (TopOn‘∪ 𝑀)) |
61 | | cnf2 21431 |
. . . . . . . . . 10
⊢ (((𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝑀 ∈ (TopOn‘∪ 𝑀)
∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶∪ 𝑀) |
62 | 33, 60, 55, 61 | syl3anc 1494 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶∪ 𝑀) |
63 | | eqid 2825 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) |
64 | 63 | fmpt2 7505 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶∪ 𝑀) |
65 | 62, 64 | sylibr 226 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀) |
66 | | rsp2 3145 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐵 ∈ ∪ 𝑀)) |
67 | 65, 66 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐵 ∈ ∪ 𝑀)) |
68 | 67 | 3impib 1148 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐵 ∈ ∪ 𝑀) |
69 | 63 | ovmpt4g 7048 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐵 ∈ ∪ 𝑀) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦) = 𝐵) |
70 | 37, 38, 68, 69 | syl3anc 1494 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦) = 𝐵) |
71 | 54, 70 | opeq12d 4633 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉 = 〈𝐴, 𝐵〉) |
72 | 71 | mpt2eq3dva 6984 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)𝑦), (𝑥(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)𝑦)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝐴, 𝐵〉)) |
73 | 29, 36, 72 | 3eqtr3a 2885 |
. 2
⊢ (𝜑 → (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝐴, 𝐵〉)) |
74 | | eqid 2825 |
. . . 4
⊢ ∪ (𝐽
×t 𝐾) =
∪ (𝐽 ×t 𝐾) |
75 | | eqid 2825 |
. . . 4
⊢ (𝑧 ∈ ∪ (𝐽
×t 𝐾)
↦ 〈((𝑥 ∈
𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) = (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) |
76 | 74, 75 | txcnmpt 21805 |
. . 3
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) → (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) |
77 | 39, 55, 76 | syl2anc 579 |
. 2
⊢ (𝜑 → (𝑧 ∈ ∪ (𝐽 ×t 𝐾) ↦ 〈((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧), ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵)‘𝑧)〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) |
78 | 73, 77 | eqeltrrd 2907 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝐴, 𝐵〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) |