| Step | Hyp | Ref
| Expression |
| 1 | | dscmet.1 |
. . . . . . 7
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if(𝑥 = 𝑦, 0, 1)) |
| 2 | 1 | dscmet 24585 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋)) |
| 3 | | metxmet 24344 |
. . . . . 6
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
| 4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝐷 ∈ (∞Met‘𝑋)) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
| 6 | 5 | elmopn 24452 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑢 ∈ (MetOpen‘𝐷) ↔ (𝑢 ⊆ 𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑤 ∈ ran (ball‘𝐷)(𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢)))) |
| 7 | 4, 6 | syl 17 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (𝑢 ∈ (MetOpen‘𝐷) ↔ (𝑢 ⊆ 𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑤 ∈ ran (ball‘𝐷)(𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢)))) |
| 8 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋) ∧ 𝑣 ∈ 𝑢) → 𝑋 ∈ 𝑉) |
| 9 | | ssel2 3978 |
. . . . . . . . . 10
⊢ ((𝑢 ⊆ 𝑋 ∧ 𝑣 ∈ 𝑢) → 𝑣 ∈ 𝑋) |
| 10 | 9 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋) ∧ 𝑣 ∈ 𝑢) → 𝑣 ∈ 𝑋) |
| 11 | 8, 10 | jca 511 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋) ∧ 𝑣 ∈ 𝑢) → (𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋)) |
| 12 | | velsn 4642 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ {𝑣} ↔ 𝑤 = 𝑣) |
| 13 | | eleq1a 2836 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝑋 → (𝑤 = 𝑣 → 𝑤 ∈ 𝑋)) |
| 14 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1) → 𝑤 ∈ 𝑋) |
| 15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝑋 → ((𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1) → 𝑤 ∈ 𝑋)) |
| 16 | | eqeq12 2754 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → (𝑥 = 𝑦 ↔ 𝑣 = 𝑤)) |
| 17 | 16 | ifbid 4549 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑤) → if(𝑥 = 𝑦, 0, 1) = if(𝑣 = 𝑤, 0, 1)) |
| 18 | | 0re 11263 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℝ |
| 19 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℝ |
| 20 | 18, 19 | ifcli 4573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ if(𝑣 = 𝑤, 0, 1) ∈ ℝ |
| 21 | 20 | elexi 3503 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(𝑣 = 𝑤, 0, 1) ∈ V |
| 22 | 17, 1, 21 | ovmpoa 7588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑣𝐷𝑤) = if(𝑣 = 𝑤, 0, 1)) |
| 23 | 22 | breq1d 5153 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → ((𝑣𝐷𝑤) < 1 ↔ if(𝑣 = 𝑤, 0, 1) < 1)) |
| 24 | 19 | ltnri 11370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ¬ 1
< 1 |
| 25 | | iffalse 4534 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝑣 = 𝑤 → if(𝑣 = 𝑤, 0, 1) = 1) |
| 26 | 25 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑣 = 𝑤 → (if(𝑣 = 𝑤, 0, 1) < 1 ↔ 1 <
1)) |
| 27 | 24, 26 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑣 = 𝑤 → ¬ if(𝑣 = 𝑤, 0, 1) < 1) |
| 28 | 27 | con4i 114 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (if(𝑣 = 𝑤, 0, 1) < 1 → 𝑣 = 𝑤) |
| 29 | | iftrue 4531 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = 𝑤 → if(𝑣 = 𝑤, 0, 1) = 0) |
| 30 | | 0lt1 11785 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 <
1 |
| 31 | 29, 30 | eqbrtrdi 5182 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝑤 → if(𝑣 = 𝑤, 0, 1) < 1) |
| 32 | 28, 31 | impbii 209 |
. . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑣 = 𝑤, 0, 1) < 1 ↔ 𝑣 = 𝑤) |
| 33 | | equcom 2017 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑤 ↔ 𝑤 = 𝑣) |
| 34 | 32, 33 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (if(𝑣 = 𝑤, 0, 1) < 1 ↔ 𝑤 = 𝑣) |
| 35 | 23, 34 | bitr2di 288 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑤 = 𝑣 ↔ (𝑣𝐷𝑤) < 1)) |
| 36 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝑋) |
| 37 | 36 | biantrurd 532 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → ((𝑣𝐷𝑤) < 1 ↔ (𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1))) |
| 38 | 35, 37 | bitrd 279 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑤 = 𝑣 ↔ (𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1))) |
| 39 | 38 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝑋 → (𝑤 ∈ 𝑋 → (𝑤 = 𝑣 ↔ (𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1)))) |
| 40 | 13, 15, 39 | pm5.21ndd 379 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ 𝑋 → (𝑤 = 𝑣 ↔ (𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1))) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋) → (𝑤 = 𝑣 ↔ (𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1))) |
| 42 | | 1xr 11320 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ* |
| 43 | | elbl 24398 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑣 ∈ 𝑋 ∧ 1 ∈ ℝ*) →
(𝑤 ∈ (𝑣(ball‘𝐷)1) ↔ (𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1))) |
| 44 | 42, 43 | mp3an3 1452 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑣 ∈ 𝑋) → (𝑤 ∈ (𝑣(ball‘𝐷)1) ↔ (𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1))) |
| 45 | 4, 44 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋) → (𝑤 ∈ (𝑣(ball‘𝐷)1) ↔ (𝑤 ∈ 𝑋 ∧ (𝑣𝐷𝑤) < 1))) |
| 46 | 41, 45 | bitr4d 282 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋) → (𝑤 = 𝑣 ↔ 𝑤 ∈ (𝑣(ball‘𝐷)1))) |
| 47 | 12, 46 | bitrid 283 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋) → (𝑤 ∈ {𝑣} ↔ 𝑤 ∈ (𝑣(ball‘𝐷)1))) |
| 48 | 47 | eqrdv 2735 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋) → {𝑣} = (𝑣(ball‘𝐷)1)) |
| 49 | | blelrn 24427 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑣 ∈ 𝑋 ∧ 1 ∈ ℝ*) →
(𝑣(ball‘𝐷)1) ∈ ran (ball‘𝐷)) |
| 50 | 42, 49 | mp3an3 1452 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑣 ∈ 𝑋) → (𝑣(ball‘𝐷)1) ∈ ran (ball‘𝐷)) |
| 51 | 4, 50 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋) → (𝑣(ball‘𝐷)1) ∈ ran (ball‘𝐷)) |
| 52 | 48, 51 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋) → {𝑣} ∈ ran (ball‘𝐷)) |
| 53 | | snssi 4808 |
. . . . . . . . . 10
⊢ (𝑣 ∈ 𝑢 → {𝑣} ⊆ 𝑢) |
| 54 | | vsnid 4663 |
. . . . . . . . . 10
⊢ 𝑣 ∈ {𝑣} |
| 55 | 53, 54 | jctil 519 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝑢 → (𝑣 ∈ {𝑣} ∧ {𝑣} ⊆ 𝑢)) |
| 56 | | eleq2 2830 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑣} → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ {𝑣})) |
| 57 | | sseq1 4009 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑣} → (𝑤 ⊆ 𝑢 ↔ {𝑣} ⊆ 𝑢)) |
| 58 | 56, 57 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑤 = {𝑣} → ((𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢) ↔ (𝑣 ∈ {𝑣} ∧ {𝑣} ⊆ 𝑢))) |
| 59 | 58 | rspcev 3622 |
. . . . . . . . 9
⊢ (({𝑣} ∈ ran (ball‘𝐷) ∧ (𝑣 ∈ {𝑣} ∧ {𝑣} ⊆ 𝑢)) → ∃𝑤 ∈ ran (ball‘𝐷)(𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢)) |
| 60 | 52, 55, 59 | syl2an 596 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋) ∧ 𝑣 ∈ 𝑢) → ∃𝑤 ∈ ran (ball‘𝐷)(𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢)) |
| 61 | 11, 60 | sylancom 588 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋) ∧ 𝑣 ∈ 𝑢) → ∃𝑤 ∈ ran (ball‘𝐷)(𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢)) |
| 62 | 61 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑢 ⊆ 𝑋) → ∀𝑣 ∈ 𝑢 ∃𝑤 ∈ ran (ball‘𝐷)(𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢)) |
| 63 | 62 | ex 412 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝑢 ⊆ 𝑋 → ∀𝑣 ∈ 𝑢 ∃𝑤 ∈ ran (ball‘𝐷)(𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))) |
| 64 | 63 | pm4.71d 561 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (𝑢 ⊆ 𝑋 ↔ (𝑢 ⊆ 𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑤 ∈ ran (ball‘𝐷)(𝑣 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢)))) |
| 65 | 7, 64 | bitr4d 282 |
. . 3
⊢ (𝑋 ∈ 𝑉 → (𝑢 ∈ (MetOpen‘𝐷) ↔ 𝑢 ⊆ 𝑋)) |
| 66 | | velpw 4605 |
. . 3
⊢ (𝑢 ∈ 𝒫 𝑋 ↔ 𝑢 ⊆ 𝑋) |
| 67 | 65, 66 | bitr4di 289 |
. 2
⊢ (𝑋 ∈ 𝑉 → (𝑢 ∈ (MetOpen‘𝐷) ↔ 𝑢 ∈ 𝒫 𝑋)) |
| 68 | 67 | eqrdv 2735 |
1
⊢ (𝑋 ∈ 𝑉 → (MetOpen‘𝐷) = 𝒫 𝑋) |