| Step | Hyp | Ref
| Expression |
| 1 | | cnmptid.j |
. . . 4
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 2 | | toponuni 22920 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 3 | | mpteq1 5235 |
. . . 4
⊢ (𝑋 = ∪
𝐽 → (𝑥 ∈ 𝑋 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉)) |
| 4 | 1, 2, 3 | 3syl 18 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉)) |
| 5 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 6 | | cnmpt11.a |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) |
| 7 | | cntop2 23249 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ Top) |
| 9 | | toptopon2 22924 |
. . . . . . . . 9
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
| 10 | 8, 9 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
| 11 | | cnf2 23257 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ 𝐾) |
| 12 | 1, 10, 6, 11 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶∪ 𝐾) |
| 13 | 12 | fvmptelcdm 7133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ∪ 𝐾) |
| 14 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴) |
| 15 | 14 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ 𝐾) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
| 16 | 5, 13, 15 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
| 17 | | cnmpt1t.b |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) |
| 18 | | cntop2 23249 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top) |
| 19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ Top) |
| 20 | | toptopon2 22924 |
. . . . . . . . 9
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
| 21 | 19, 20 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
| 22 | | cnf2 23257 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶∪ 𝐿) |
| 23 | 1, 21, 17, 22 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶∪ 𝐿) |
| 24 | 23 | fvmptelcdm 7133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ ∪ 𝐿) |
| 25 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ 𝐵) |
| 26 | 25 | fvmpt2 7027 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐵 ∈ ∪ 𝐿) → ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥) = 𝐵) |
| 27 | 5, 24, 26 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥) = 𝐵) |
| 28 | 16, 27 | opeq12d 4881 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉 = 〈𝐴, 𝐵〉) |
| 29 | 28 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉)) |
| 30 | 4, 29 | eqtr3d 2779 |
. 2
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉)) |
| 31 | | eqid 2737 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 32 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉 |
| 33 | | nffvmpt1 6917 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦) |
| 34 | | nffvmpt1 6917 |
. . . . . 6
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦) |
| 35 | 33, 34 | nfop 4889 |
. . . . 5
⊢
Ⅎ𝑥〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦)〉 |
| 36 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦)) |
| 37 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦)) |
| 38 | 36, 37 | opeq12d 4881 |
. . . . 5
⊢ (𝑥 = 𝑦 → 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉 = 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦)〉) |
| 39 | 32, 35, 38 | cbvmpt 5253 |
. . . 4
⊢ (𝑥 ∈ ∪ 𝐽
↦ 〈((𝑥 ∈
𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) = (𝑦 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑦), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑦)〉) |
| 40 | 31, 39 | txcnmpt 23632 |
. . 3
⊢ (((𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾) ∧ (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) → (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |
| 41 | 6, 17, 40 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐽 ↦ 〈((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥), ((𝑥 ∈ 𝑋 ↦ 𝐵)‘𝑥)〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |
| 42 | 30, 41 | eqeltrrd 2842 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) |