| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tmdcn2.2 | . . . . 5
⊢ 𝐽 = (TopOpen‘𝐺) | 
| 2 |  | tmdcn2.1 | . . . . 5
⊢ 𝐵 = (Base‘𝐺) | 
| 3 | 1, 2 | tmdtopon 24090 | . . . 4
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵)) | 
| 4 | 3 | ad2antrr 726 | . . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝐽 ∈ (TopOn‘𝐵)) | 
| 5 |  | eqid 2736 | . . . . . 6
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) | 
| 6 | 1, 5 | tmdcn 24092 | . . . . 5
⊢ (𝐺 ∈ TopMnd →
(+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | 
| 7 | 6 | ad2antrr 726 | . . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | 
| 8 |  | simpr1 1194 | . . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝑋 ∈ 𝐵) | 
| 9 |  | simpr2 1195 | . . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝑌 ∈ 𝐵) | 
| 10 | 8, 9 | opelxpd 5723 | . . . . 5
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) | 
| 11 |  | txtopon 23600 | . . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝐵) ∧ 𝐽 ∈ (TopOn‘𝐵)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵))) | 
| 12 | 4, 4, 11 | syl2anc 584 | . . . . . 6
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵))) | 
| 13 |  | toponuni 22921 | . . . . . 6
⊢ ((𝐽 ×t 𝐽) ∈ (TopOn‘(𝐵 × 𝐵)) → (𝐵 × 𝐵) = ∪ (𝐽 ×t 𝐽)) | 
| 14 | 12, 13 | syl 17 | . . . . 5
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝐵 × 𝐵) = ∪ (𝐽 ×t 𝐽)) | 
| 15 | 10, 14 | eleqtrd 2842 | . . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 〈𝑋, 𝑌〉 ∈ ∪
(𝐽 ×t
𝐽)) | 
| 16 |  | eqid 2736 | . . . . 5
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) | 
| 17 | 16 | cncnpi 23287 | . . . 4
⊢
(((+𝑓‘𝐺) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ 〈𝑋, 𝑌〉 ∈ ∪
(𝐽 ×t
𝐽)) →
(+𝑓‘𝐺) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝑋, 𝑌〉)) | 
| 18 | 7, 15, 17 | syl2anc 584 | . . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (+𝑓‘𝐺) ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘〈𝑋, 𝑌〉)) | 
| 19 |  | simplr 768 | . . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → 𝑈 ∈ 𝐽) | 
| 20 |  | tmdcn2.3 | . . . . . 6
⊢  + =
(+g‘𝐺) | 
| 21 | 2, 20, 5 | plusfval 18661 | . . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) | 
| 22 | 8, 9, 21 | syl2anc 584 | . . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝑋(+𝑓‘𝐺)𝑌) = (𝑋 + 𝑌)) | 
| 23 |  | simpr3 1196 | . . . 4
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝑋 + 𝑌) ∈ 𝑈) | 
| 24 | 22, 23 | eqeltrd 2840 | . . 3
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → (𝑋(+𝑓‘𝐺)𝑌) ∈ 𝑈) | 
| 25 | 4, 4, 18, 19, 8, 9, 24 | txcnpi 23617 | . 2
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈))) | 
| 26 |  | dfss3 3971 | . . . . . . 7
⊢ ((𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈) ↔ ∀𝑧 ∈ (𝑢 × 𝑣)𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈)) | 
| 27 |  | eleq1 2828 | . . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ 〈𝑥, 𝑦〉 ∈ (◡(+𝑓‘𝐺) “ 𝑈))) | 
| 28 | 2, 5 | plusffn 18663 | . . . . . . . . . 10
⊢
(+𝑓‘𝐺) Fn (𝐵 × 𝐵) | 
| 29 |  | elpreima 7077 | . . . . . . . . . 10
⊢
((+𝑓‘𝐺) Fn (𝐵 × 𝐵) → (〈𝑥, 𝑦〉 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈))) | 
| 30 | 28, 29 | ax-mp 5 | . . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈)) | 
| 31 | 27, 30 | bitrdi 287 | . . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈))) | 
| 32 | 31 | ralxp 5851 | . . . . . . 7
⊢
(∀𝑧 ∈
(𝑢 × 𝑣)𝑧 ∈ (◡(+𝑓‘𝐺) “ 𝑈) ↔ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈)) | 
| 33 | 26, 32 | bitri 275 | . . . . . 6
⊢ ((𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈) ↔ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈)) | 
| 34 |  | opelxp 5720 | . . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) | 
| 35 |  | df-ov 7435 | . . . . . . . . . . 11
⊢ (𝑥(+𝑓‘𝐺)𝑦) = ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) | 
| 36 | 2, 20, 5 | plusfval 18661 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+𝑓‘𝐺)𝑦) = (𝑥 + 𝑦)) | 
| 37 | 35, 36 | eqtr3id 2790 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) = (𝑥 + 𝑦)) | 
| 38 | 34, 37 | sylbi 217 | . . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) → ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) = (𝑥 + 𝑦)) | 
| 39 | 38 | eleq1d 2825 | . . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) →
(((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈 ↔ (𝑥 + 𝑦) ∈ 𝑈)) | 
| 40 | 39 | biimpa 476 | . . . . . . 7
⊢
((〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈) → (𝑥 + 𝑦) ∈ 𝑈) | 
| 41 | 40 | 2ralimi 3122 | . . . . . 6
⊢
(∀𝑥 ∈
𝑢 ∀𝑦 ∈ 𝑣 (〈𝑥, 𝑦〉 ∈ (𝐵 × 𝐵) ∧ ((+𝑓‘𝐺)‘〈𝑥, 𝑦〉) ∈ 𝑈) → ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈) | 
| 42 | 33, 41 | sylbi 217 | . . . . 5
⊢ ((𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈) → ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈) | 
| 43 | 42 | 3anim3i 1154 | . . . 4
⊢ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈)) → (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) | 
| 44 | 43 | reximi 3083 | . . 3
⊢
(∃𝑣 ∈
𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈)) → ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) | 
| 45 | 44 | reximi 3083 | . 2
⊢
(∃𝑢 ∈
𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡(+𝑓‘𝐺) “ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) | 
| 46 | 25, 45 | syl 17 | 1
⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) |