Step | Hyp | Ref
| Expression |
1 | | cnmptid.j |
. . . 4
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | toponuni 20542 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
3 | | mpteq1 4665 |
. . . 4
⊢ (𝑋 = ∪
𝐽 → (𝑥 ∈ 𝑋 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉)) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉)) |
5 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
6 | | cnmpt11.a |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) |
7 | | cntop2 20855 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ Top) |
9 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝐾 =
∪ 𝐾 |
10 | 9 | toptopon 20548 |
. . . . . . . . . 10
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
11 | 8, 10 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
12 | | cnf2 20863 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ 𝐾) |
13 | 1, 11, 6, 12 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ 𝐾) |
14 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴) |
15 | 14 | fmpt 6289 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 𝐴 ∈ ∪ 𝐾 ↔ (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ 𝐾) |
16 | 13, 15 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐴 ∈ ∪ 𝐾) |
17 | 16 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ 𝐾) |
18 | 14 | fvmpt2 6200 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ 𝐾) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
19 | 5, 17, 18 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
20 | | cnmpt1t.b |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) |
21 | | cntop2 20855 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ Top) |
23 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝐿 =
∪ 𝐿 |
24 | 23 | toptopon 20548 |
. . . . . . . . . 10
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
25 | 22, 24 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
26 | | cnf2 20863 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶∪ 𝐿) |
27 | 1, 25, 20, 26 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶∪ 𝐿) |
28 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ 𝐵) |
29 | 28 | fmpt 6289 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 𝐵 ∈ ∪ 𝐿 ↔ (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶∪ 𝐿) |
30 | 27, 29 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐵 ∈ ∪ 𝐿) |
31 | 30 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ∪ 𝐿) |
32 | 28 | fvmpt2 6200 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐵 ∈ ∪ 𝐿) → ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥) = 𝐵) |
33 | 5, 31, 32 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥) = 𝐵) |
34 | 19, 33 | opeq12d 4348 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉 = 〈𝐴, 𝐵〉) |
35 | 34 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉)) |
36 | 4, 35 | eqtr3d 2646 |
. 2
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉)) |
37 | | eqid 2610 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
38 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉 |
39 | | nffvmpt1 6111 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦) |
40 | | nffvmpt1 6111 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦) |
41 | 39, 40 | nfop 4356 |
. . . . 5
⊢
Ⅎ𝑥〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦)〉 |
42 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦)) |
43 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦)) |
44 | 42, 43 | opeq12d 4348 |
. . . . 5
⊢ (𝑥 = 𝑦 → 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉 = 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦)〉) |
45 | 38, 41, 44 | cbvmpt 4677 |
. . . 4
⊢ (𝑥 ∈ ∪ 𝐽
↦ 〈((𝑥 ∈
𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑦 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦)〉) |
46 | 37, 45 | txcnmpt 21237 |
. . 3
⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾) ∧ (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) → (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |
47 | 6, 20, 46 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |
48 | 36, 47 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |