Step | Hyp | Ref
| Expression |
1 | | tmdcn2.2 |
. . . . 5
⊢ 𝐽 = (TopOpen‘𝐺) |
2 | | tmdcn2.1 |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
3 | 1, 2 | tmdtopon 21885 |
. . . 4
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵)) |
4 | 3 | ad2antrr 762 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝐽 ∈ (TopOn‘𝐵)) |
5 | | eqid 2622 |
. . . . . 6
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) |
6 | 1, 5 | tmdcn 21887 |
. . . . 5
⊢ (𝐺 ∈ TopMnd →
(+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
7 | 6 | ad2antrr 762 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
8 | | simpr1 1067 |
. . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝑋 ∈ 𝐵) |
9 | | simpr2 1068 |
. . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝑌 ∈ 𝐵) |
10 | | opelxpi 5148 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
11 | 8, 9, 10 | syl2anc 693 |
. . . . 5
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
12 | | txtopon 21394 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐽 ∈ (TopOn‘𝐵)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵))) |
13 | 4, 4, 12 | syl2anc 693 |
. . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵))) |
14 | | toponuni 20719 |
. . . . . 6
⊢ ((𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵)) → (𝐵 × 𝐵) = ∪ (𝐽 ×t 𝐽)) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝐵 × 𝐵) = ∪ (𝐽 ×t 𝐽)) |
16 | 11, 15 | eleqtrd 2703 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 〈𝑋, 𝑌〉 ∈ ∪
(𝐽 ×t
𝐽)) |
17 | | eqid 2622 |
. . . . 5
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
18 | 17 | cncnpi 21082 |
. . . 4
⊢
(((+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ 〈𝑋, 𝑌〉 ∈ ∪
(𝐽 ×t
𝐽)) →
(+𝑓‘𝐺) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝑋, 𝑌〉)) |
19 | 7, 16, 18 | syl2anc 693 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (+𝑓‘𝐺) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝑋, 𝑌〉)) |
20 | | simplr 792 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝑈 ∈ 𝐽) |
21 | | tmdcn2.3 |
. . . . . 6
⊢ + =
(+g‘𝐺) |
22 | 2, 21, 5 | plusfval 17248 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) |
23 | 8, 9, 22 | syl2anc 693 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) |
24 | | simpr3 1069 |
. . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝑋 + 𝑌) ∈ 𝑈) |
25 | 23, 24 | eqeltrd 2701 |
. . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝑋(+𝑓‘𝐺)𝑌) ∈ 𝑈) |
26 | 4, 4, 19, 20, 8, 9, 25 | txcnpi 21411 |
. 2
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈))) |
27 | | dfss3 3592 |
. . . . . . 7
⊢ ((𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈) ↔ ∀𝑧 ∈ (𝑢 × 𝑣)𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈)) |
28 | | eleq1 2689 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ 〈𝑥, 𝑦〉 ∈ (◡(+𝑓‘𝐺) “ 𝑈))) |
29 | 2, 5 | plusffn 17250 |
. . . . . . . . . 10
⊢
(+𝑓‘𝐺) Fn (𝐵 × 𝐵) |
30 | | elpreima 6337 |
. . . . . . . . . 10
⊢
((+𝑓‘𝐺) Fn (𝐵 × 𝐵) → (〈𝑥, 𝑦〉 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈))) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈)) |
32 | 28, 31 | syl6bb 276 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈))) |
33 | 32 | ralxp 5263 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝑢 × 𝑣)𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈)) |
34 | 27, 33 | bitri 264 |
. . . . . 6
⊢ ((𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈) ↔ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈)) |
35 | | opelxp 5146 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
36 | | df-ov 6653 |
. . . . . . . . . . 11
⊢ (𝑥(+𝑓‘𝐺)𝑦) = ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) |
37 | 2, 21, 5 | plusfval 17248 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+𝑓‘𝐺)𝑦) = (𝑥 + 𝑦)) |
38 | 36, 37 | syl5eqr 2670 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) = (𝑥 + 𝑦)) |
39 | 35, 38 | sylbi 207 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) → ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) = (𝑥 + 𝑦)) |
40 | 39 | eleq1d 2686 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) →
(((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈 ↔ (𝑥 + 𝑦) ∈ 𝑈)) |
41 | 40 | biimpa 501 |
. . . . . . 7
⊢
((〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈) → (𝑥 + 𝑦) ∈ 𝑈) |
42 | 41 | 2ralimi 2953 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑢 ∀𝑦 ∈ 𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈) → ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈) |
43 | 34, 42 | sylbi 207 |
. . . . 5
⊢ ((𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈) → ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈) |
44 | 43 | 3anim3i 1250 |
. . . 4
⊢ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈)) → (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) |
45 | 44 | reximi 3011 |
. . 3
⊢
(∃𝑣 ∈
𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈)) → ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) |
46 | 45 | reximi 3011 |
. 2
⊢
(∃𝑢 ∈
𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) |
47 | 26, 46 | syl 17 |
1
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) |