Proof of Theorem cnmpt2plusg
Step | Hyp | Ref
| Expression |
1 | | cnmpt1plusg.k |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) |
2 | | cnmpt2plusg.l |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) |
3 | | txtopon 22740 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑌)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌))) |
4 | 1, 2, 3 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌))) |
5 | | cnmpt1plusg.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ TopMnd) |
6 | | tgpcn.j |
. . . . . . . . . . 11
⊢ 𝐽 = (TopOpen‘𝐺) |
7 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(Base‘𝐺) =
(Base‘𝐺) |
8 | 6, 7 | tmdtopon 23230 |
. . . . . . . . . 10
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈
(TopOn‘(Base‘𝐺))) |
9 | 5, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝐺))) |
10 | | cnmpt2plusg.a |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) |
11 | | cnf2 22398 |
. . . . . . . . 9
⊢ (((𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐽 ∈ (TopOn‘(Base‘𝐺)) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶(Base‘𝐺)) |
12 | 4, 9, 10, 11 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶(Base‘𝐺)) |
13 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) |
14 | 13 | fmpo 7908 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ (Base‘𝐺) ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴):(𝑋 × 𝑌)⟶(Base‘𝐺)) |
15 | 12, 14 | sylibr 233 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴 ∈ (Base‘𝐺)) |
16 | 15 | r19.21bi 3134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ (Base‘𝐺)) |
17 | 16 | r19.21bi 3134 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ (Base‘𝐺)) |
18 | 17 | 3impa 1109 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ (Base‘𝐺)) |
19 | | cnmpt2plusg.b |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) |
20 | | cnf2 22398 |
. . . . . . . . 9
⊢ (((𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐽 ∈ (TopOn‘(Base‘𝐺)) ∧ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶(Base‘𝐺)) |
21 | 4, 9, 19, 20 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶(Base‘𝐺)) |
22 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) |
23 | 22 | fmpo 7908 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ (Base‘𝐺) ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵):(𝑋 × 𝑌)⟶(Base‘𝐺)) |
24 | 21, 23 | sylibr 233 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐵 ∈ (Base‘𝐺)) |
25 | 24 | r19.21bi 3134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐵 ∈ (Base‘𝐺)) |
26 | 25 | r19.21bi 3134 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝐵 ∈ (Base‘𝐺)) |
27 | 26 | 3impa 1109 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝐵 ∈ (Base‘𝐺)) |
28 | | cnmpt1plusg.p |
. . . . 5
⊢ + =
(+g‘𝐺) |
29 | | eqid 2738 |
. . . . 5
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) |
30 | 7, 28, 29 | plusfval 18331 |
. . . 4
⊢ ((𝐴 ∈ (Base‘𝐺) ∧ 𝐵 ∈ (Base‘𝐺)) → (𝐴(+𝑓‘𝐺)𝐵) = (𝐴 + 𝐵)) |
31 | 18, 27, 30 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (𝐴(+𝑓‘𝐺)𝐵) = (𝐴 + 𝐵)) |
32 | 31 | mpoeq3dva 7352 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴(+𝑓‘𝐺)𝐵)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 + 𝐵))) |
33 | 6, 29 | tmdcn 23232 |
. . . 4
⊢ (𝐺 ∈ TopMnd →
(+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
34 | 5, 33 | syl 17 |
. . 3
⊢ (𝜑 →
(+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
35 | 1, 2, 10, 19, 34 | cnmpt22f 22824 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴(+𝑓‘𝐺)𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) |
36 | 32, 35 | eqeltrrd 2840 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 + 𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) |