Step | Hyp | Ref
| Expression |
1 | | tmdcn2.2 |
. . . . 5
⊢ 𝐽 = (TopOpen‘𝐺) |
2 | | tmdcn2.1 |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
3 | 1, 2 | tmdtopon 21695 |
. . . 4
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵)) |
4 | 3 | ad2antrr 758 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝐽 ∈ (TopOn‘𝐵)) |
5 | | eqid 2610 |
. . . . . 6
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) |
6 | 1, 5 | tmdcn 21697 |
. . . . 5
⊢ (𝐺 ∈ TopMnd →
(+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
7 | 6 | ad2antrr 758 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
8 | | simpr1 1060 |
. . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝑋 ∈ 𝐵) |
9 | | simpr2 1061 |
. . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝑌 ∈ 𝐵) |
10 | | opelxpi 5072 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
11 | 8, 9, 10 | syl2anc 691 |
. . . . 5
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
12 | | txtopon 21204 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐽 ∈ (TopOn‘𝐵)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵))) |
13 | 4, 4, 12 | syl2anc 691 |
. . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵))) |
14 | | toponuni 20542 |
. . . . . 6
⊢ ((𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵)) → (𝐵 × 𝐵) = ∪ (𝐽 ×t 𝐽)) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝐵 × 𝐵) = ∪ (𝐽 ×t 𝐽)) |
16 | 11, 15 | eleqtrd 2690 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 〈𝑋, 𝑌〉 ∈ ∪
(𝐽 ×t
𝐽)) |
17 | | eqid 2610 |
. . . . 5
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
18 | 17 | cncnpi 20892 |
. . . 4
⊢
(((+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ 〈𝑋, 𝑌〉 ∈ ∪
(𝐽 ×t
𝐽)) →
(+𝑓‘𝐺) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝑋, 𝑌〉)) |
19 | 7, 16, 18 | syl2anc 691 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (+𝑓‘𝐺) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝑋, 𝑌〉)) |
20 | | simplr 788 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝑈 ∈ 𝐽) |
21 | | tmdcn2.3 |
. . . . . 6
⊢ + =
(+g‘𝐺) |
22 | 2, 21, 5 | plusfval 17071 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) |
23 | 8, 9, 22 | syl2anc 691 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) |
24 | | simpr3 1062 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝑋 + 𝑌) ∈ 𝑈) |
25 | 23, 24 | eqeltrd 2688 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝑋(+𝑓‘𝐺)𝑌) ∈ 𝑈) |
26 | 4, 4, 19, 20, 8, 9, 25 | txcnpi 21221 |
. 2
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈))) |
27 | | dfss3 3558 |
. . . . . . 7
⊢ ((𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈) ↔ ∀𝑧 ∈ (𝑢 × 𝑣)𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈)) |
28 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ 〈𝑥, 𝑦〉 ∈ (◡(+𝑓‘𝐺) “ 𝑈))) |
29 | 2, 5 | plusffn 17073 |
. . . . . . . . . 10
⊢
(+𝑓‘𝐺) Fn (𝐵 × 𝐵) |
30 | | elpreima 6245 |
. . . . . . . . . 10
⊢
((+𝑓‘𝐺) Fn (𝐵 × 𝐵) → (〈𝑥, 𝑦〉 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈))) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈)) |
32 | 28, 31 | syl6bb 275 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈))) |
33 | 32 | ralxp 5185 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝑢 × 𝑣)𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈)) |
34 | 27, 33 | bitri 263 |
. . . . . 6
⊢ ((𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈) ↔ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈)) |
35 | | opelxp 5070 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
36 | | df-ov 6552 |
. . . . . . . . . . . 12
⊢ (𝑥(+𝑓‘𝐺)𝑦) = ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) |
37 | 2, 21, 5 | plusfval 17071 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+𝑓‘𝐺)𝑦) = (𝑥 + 𝑦)) |
38 | 36, 37 | syl5eqr 2658 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) = (𝑥 + 𝑦)) |
39 | 35, 38 | sylbi 206 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) → ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) = (𝑥 + 𝑦)) |
40 | 39 | eleq1d 2672 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) →
(((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈 ↔ (𝑥 + 𝑦) ∈ 𝑈)) |
41 | 40 | biimpa 500 |
. . . . . . . 8
⊢
((〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈) → (𝑥 + 𝑦) ∈ 𝑈) |
42 | 41 | ralimi 2936 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈) → ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈) |
43 | 42 | ralimi 2936 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑢 ∀𝑦 ∈ 𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈) → ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈) |
44 | 34, 43 | sylbi 206 |
. . . . 5
⊢ ((𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈) → ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈) |
45 | 44 | 3anim3i 1243 |
. . . 4
⊢ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈)) → (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) |
46 | 45 | reximi 2994 |
. . 3
⊢
(∃𝑣 ∈
𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈)) → ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) |
47 | 46 | reximi 2994 |
. 2
⊢
(∃𝑢 ∈
𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) |
48 | 26, 47 | syl 17 |
1
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) |