Step | Hyp | Ref
| Expression |
1 | | nfcv 2907 |
. . . . 5
⊢
Ⅎ𝑥𝑌 |
2 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑥𝑣 |
3 | | nfmpo2 7313 |
. . . . . 6
⊢
Ⅎ𝑥(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) |
4 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑥𝑤 |
5 | 2, 3, 4 | nfov 7264 |
. . . . 5
⊢
Ⅎ𝑥(𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) |
6 | 1, 5 | nfmpt 5168 |
. . . 4
⊢
Ⅎ𝑥(𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) |
7 | | nfcv 2907 |
. . . 4
⊢
Ⅎ𝑤(𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥)) |
8 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑦𝑣 |
9 | | nfmpo1 7312 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) |
10 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑦𝑤 |
11 | 8, 9, 10 | nfov 7264 |
. . . . . 6
⊢
Ⅎ𝑦(𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) |
12 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑣(𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) |
13 | | oveq1 7241 |
. . . . . 6
⊢ (𝑣 = 𝑦 → (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) = (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) |
14 | 11, 12, 13 | cbvmpt 5172 |
. . . . 5
⊢ (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) = (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) |
15 | | oveq2 7242 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) = (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥)) |
16 | 15 | mpteq2dv 5167 |
. . . . 5
⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) = (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥))) |
17 | 14, 16 | syl5eq 2792 |
. . . 4
⊢ (𝑤 = 𝑥 → (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) = (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥))) |
18 | 6, 7, 17 | cbvmpt 5172 |
. . 3
⊢ (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥))) |
19 | | simpr 488 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
20 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝑥 ∈ 𝑋) |
21 | | cnmpt2k.k |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
22 | | cnmpt2k.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
23 | | txtopon 22519 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝐾 ×t 𝐽) ∈ (TopOn‘(𝑌 × 𝑋))) |
24 | 21, 22, 23 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾 ×t 𝐽) ∈ (TopOn‘(𝑌 × 𝑋))) |
25 | | cnmpt2k.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
26 | | cntop2 22169 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿) → 𝐿 ∈ Top) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ Top) |
28 | | toptopon2 21846 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
29 | 27, 28 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
30 | 22, 21, 25 | cnmptcom 22606 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐾 ×t 𝐽) Cn 𝐿)) |
31 | | cnf2 22177 |
. . . . . . . . . . 11
⊢ (((𝐾 ×t 𝐽) ∈ (TopOn‘(𝑌 × 𝑋)) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐾 ×t 𝐽) Cn 𝐿)) → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴):(𝑌 × 𝑋)⟶∪ 𝐿) |
32 | 24, 29, 30, 31 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴):(𝑌 × 𝑋)⟶∪ 𝐿) |
33 | | eqid 2739 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) |
34 | 33 | fmpo 7859 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑌 ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐿 ↔ (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴):(𝑌 × 𝑋)⟶∪ 𝐿) |
35 | 32, 34 | sylibr 237 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ 𝑌 ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐿) |
36 | 35 | r19.21bi 3133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐿) |
37 | 36 | r19.21bi 3133 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ 𝐿) |
38 | 37 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ ∪ 𝐿) |
39 | 33 | ovmpt4g 7377 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ 𝐿) → (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥) = 𝐴) |
40 | 19, 20, 38, 39 | syl3anc 1373 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥) = 𝐴) |
41 | 40 | mpteq2dva 5166 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥)) = (𝑦 ∈ 𝑌 ↦ 𝐴)) |
42 | 41 | mpteq2dva 5166 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑦(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑥))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))) |
43 | 18, 42 | syl5eq 2792 |
. 2
⊢ (𝜑 → (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))) |
44 | | eqid 2739 |
. . . . 5
⊢ (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ 〈𝑣, 𝑤〉)) = (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ 〈𝑣, 𝑤〉)) |
45 | 44 | xkoinjcn 22615 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ 〈𝑣, 𝑤〉)) ∈ (𝐽 Cn ((𝐾 ×t 𝐽) ↑ko 𝐾))) |
46 | 22, 21, 45 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ 〈𝑣, 𝑤〉)) ∈ (𝐽 Cn ((𝐾 ×t 𝐽) ↑ko 𝐾))) |
47 | 32 | feqmptd 6801 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑧 ∈ (𝑌 × 𝑋) ↦ ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑧))) |
48 | 47, 30 | eqeltrrd 2841 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝑌 × 𝑋) ↦ ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑧)) ∈ ((𝐾 ×t 𝐽) Cn 𝐿)) |
49 | | fveq2 6738 |
. . . 4
⊢ (𝑧 = 〈𝑣, 𝑤〉 → ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑧) = ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘〈𝑣, 𝑤〉)) |
50 | | df-ov 7237 |
. . . 4
⊢ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤) = ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘〈𝑣, 𝑤〉) |
51 | 49, 50 | eqtr4di 2798 |
. . 3
⊢ (𝑧 = 〈𝑣, 𝑤〉 → ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑧) = (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤)) |
52 | 22, 21, 24, 46, 48, 51 | cnmptk1 22609 |
. 2
⊢ (𝜑 → (𝑤 ∈ 𝑋 ↦ (𝑣 ∈ 𝑌 ↦ (𝑣(𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴)𝑤))) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) |
53 | 43, 52 | eqeltrrd 2841 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) |