Step | Hyp | Ref
| Expression |
1 | | nfcv 2969 |
. . . . 5
⊢
Ⅎ𝑥𝑌 |
2 | | nfcv 2969 |
. . . . . 6
⊢
Ⅎ𝑥𝑣 |
3 | | nfmpt22 6988 |
. . . . . 6
⊢
Ⅎ𝑥(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) |
4 | | nfcv 2969 |
. . . . . 6
⊢
Ⅎ𝑥𝑤 |
5 | 2, 3, 4 | nfov 6940 |
. . . . 5
⊢
Ⅎ𝑥(𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) |
6 | 1, 5 | nfmpt 4971 |
. . . 4
⊢
Ⅎ𝑥(𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) |
7 | | nfcv 2969 |
. . . 4
⊢
Ⅎ𝑤(𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥)) |
8 | | nfcv 2969 |
. . . . . . 7
⊢
Ⅎ𝑦𝑣 |
9 | | nfmpt21 6987 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) |
10 | | nfcv 2969 |
. . . . . . 7
⊢
Ⅎ𝑦𝑤 |
11 | 8, 9, 10 | nfov 6940 |
. . . . . 6
⊢
Ⅎ𝑦(𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) |
12 | | nfcv 2969 |
. . . . . 6
⊢
Ⅎ𝑣(𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) |
13 | | oveq1 6917 |
. . . . . 6
⊢ (𝑣 = 𝑦 → (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) = (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) |
14 | 11, 12, 13 | cbvmpt 4974 |
. . . . 5
⊢ (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) = (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) |
15 | | oveq2 6918 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) = (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥)) |
16 | 15 | mpteq2dv 4970 |
. . . . 5
⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) = (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥))) |
17 | 14, 16 | syl5eq 2873 |
. . . 4
⊢ (𝑤 = 𝑥 → (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) = (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥))) |
18 | 6, 7, 17 | cbvmpt 4974 |
. . 3
⊢ (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥))) |
19 | | simpr 479 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
20 | | simplr 785 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝑥 ∈ 𝑋) |
21 | | cnmpt2k.k |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
22 | | cnmpt2k.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
23 | | txtopon 21772 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝐾 ×t 𝐽) ∈ (TopOn‘(𝑌 × 𝑋))) |
24 | 21, 22, 23 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾 ×t 𝐽) ∈ (TopOn‘(𝑌 × 𝑋))) |
25 | | cnmpt2k.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
26 | | cntop2 21423 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) → 𝐿 ∈ Top) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ Top) |
28 | | eqid 2825 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐿 =
∪ 𝐿 |
29 | 28 | toptopon 21099 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
30 | 27, 29 | sylib 210 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
31 | 22, 21, 25 | cnmptcom 21859 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐾 ×t 𝐽) Cn 𝐿)) |
32 | | cnf2 21431 |
. . . . . . . . . . 11
⊢ (((𝐾 ×t 𝐽) ∈ (TopOn‘(𝑌 × 𝑋)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐾 ×t 𝐽) Cn 𝐿)) → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴):(𝑌 × 𝑋)⟶∪ 𝐿) |
33 | 24, 30, 31, 32 | syl3anc 1494 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴):(𝑌 × 𝑋)⟶∪ 𝐿) |
34 | | eqid 2825 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) |
35 | 34 | fmpt2 7505 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑌 ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐿 ↔ (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴):(𝑌 × 𝑋)⟶∪ 𝐿) |
36 | 33, 35 | sylibr 226 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐿) |
37 | 36 | r19.21bi 3141 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐿) |
38 | 37 | r19.21bi 3141 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ 𝐿) |
39 | 38 | an32s 642 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ ∪ 𝐿) |
40 | 34 | ovmpt4g 7048 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ 𝐿) → (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥) = 𝐴) |
41 | 19, 20, 39, 40 | syl3anc 1494 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥) = 𝐴) |
42 | 41 | mpteq2dva 4969 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥)) = (𝑦 ∈ 𝑌 ↦ 𝐴)) |
43 | 42 | mpteq2dva 4969 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))) |
44 | 18, 43 | syl5eq 2873 |
. 2
⊢ (𝜑 → (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))) |
45 | | eqid 2825 |
. . . . 5
⊢ (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ 〈𝑣, 𝑤〉)) = (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ 〈𝑣, 𝑤〉)) |
46 | 45 | xkoinjcn 21868 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ 〈𝑣, 𝑤〉)) ∈ (𝐽 Cn ((𝐾 ×t 𝐽) ^ko 𝐾))) |
47 | 22, 21, 46 | syl2anc 579 |
. . 3
⊢ (𝜑 → (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ 〈𝑣, 𝑤〉)) ∈ (𝐽 Cn ((𝐾 ×t 𝐽) ^ko 𝐾))) |
48 | 33 | feqmptd 6500 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑧 ∈ (𝑌 × 𝑋) ↦ ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑧))) |
49 | 48, 31 | eqeltrrd 2907 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝑌 × 𝑋) ↦ ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑧)) ∈ ((𝐾 ×t 𝐽) Cn 𝐿)) |
50 | | fveq2 6437 |
. . . 4
⊢ (𝑧 = 〈𝑣, 𝑤〉 → ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑧) = ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘〈𝑣, 𝑤〉)) |
51 | | df-ov 6913 |
. . . 4
⊢ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) = ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘〈𝑣, 𝑤〉) |
52 | 50, 51 | syl6eqr 2879 |
. . 3
⊢ (𝑧 = 〈𝑣, 𝑤〉 → ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑧) = (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) |
53 | 22, 21, 24, 47, 49, 52 | cnmptk1 21862 |
. 2
⊢ (𝜑 → (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤))) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
54 | 44, 53 | eqeltrrd 2907 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |