Proof of Theorem metnrmlem1a
| Step | Hyp | Ref
| Expression |
| 1 | | metnrmlem.4 |
. . . . . 6
⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (𝑆 ∩ 𝑇) = ∅) |
| 3 | | inelcm 4465 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑇) → (𝑆 ∩ 𝑇) ≠ ∅) |
| 4 | 3 | expcom 413 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑇 → (𝐴 ∈ 𝑆 → (𝑆 ∩ 𝑇) ≠ ∅)) |
| 5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (𝐴 ∈ 𝑆 → (𝑆 ∩ 𝑇) ≠ ∅)) |
| 6 | 5 | necon2bd 2956 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → ((𝑆 ∩ 𝑇) = ∅ → ¬ 𝐴 ∈ 𝑆)) |
| 7 | 2, 6 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → ¬ 𝐴 ∈ 𝑆) |
| 8 | | eqcom 2744 |
. . . . . 6
⊢ (0 =
(𝐹‘𝐴) ↔ (𝐹‘𝐴) = 0) |
| 9 | | metnrmlem.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
| 10 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝐷 ∈ (∞Met‘𝑋)) |
| 11 | | metnrmlem.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽)) |
| 12 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝑆 ∈ (Clsd‘𝐽)) |
| 13 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 14 | 13 | cldss 23037 |
. . . . . . . . 9
⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ ∪ 𝐽) |
| 15 | 12, 14 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝑆 ⊆ ∪ 𝐽) |
| 16 | | metdscn.j |
. . . . . . . . . 10
⊢ 𝐽 = (MetOpen‘𝐷) |
| 17 | 16 | mopnuni 24451 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
| 18 | 10, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝑋 = ∪ 𝐽) |
| 19 | 15, 18 | sseqtrrd 4021 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝑆 ⊆ 𝑋) |
| 20 | | metnrmlem.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽)) |
| 21 | 20 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝑇 ∈ (Clsd‘𝐽)) |
| 22 | 13 | cldss 23037 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (Clsd‘𝐽) → 𝑇 ⊆ ∪ 𝐽) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝑇 ⊆ ∪ 𝐽) |
| 24 | 23, 18 | sseqtrrd 4021 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝑇 ⊆ 𝑋) |
| 25 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝐴 ∈ 𝑇) |
| 26 | 24, 25 | sseldd 3984 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝐴 ∈ 𝑋) |
| 27 | | metdscn.f |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, <
)) |
| 28 | 27, 16 | metdseq0 24876 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆))) |
| 29 | 10, 19, 26, 28 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → ((𝐹‘𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆))) |
| 30 | 8, 29 | bitrid 283 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (0 = (𝐹‘𝐴) ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆))) |
| 31 | | cldcls 23050 |
. . . . . . 7
⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆) |
| 32 | 12, 31 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → ((cls‘𝐽)‘𝑆) = 𝑆) |
| 33 | 32 | eleq2d 2827 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ 𝐴 ∈ 𝑆)) |
| 34 | 30, 33 | bitrd 279 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (0 = (𝐹‘𝐴) ↔ 𝐴 ∈ 𝑆)) |
| 35 | 7, 34 | mtbird 325 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → ¬ 0 = (𝐹‘𝐴)) |
| 36 | 27 | metdsf 24870 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
| 37 | 10, 19, 36 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 𝐹:𝑋⟶(0[,]+∞)) |
| 38 | 37, 26 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (𝐹‘𝐴) ∈ (0[,]+∞)) |
| 39 | | elxrge0 13497 |
. . . . . . 7
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) ↔ ((𝐹‘𝐴) ∈ ℝ* ∧ 0 ≤
(𝐹‘𝐴))) |
| 40 | 39 | simprbi 496 |
. . . . . 6
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹‘𝐴)) |
| 41 | 38, 40 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 0 ≤ (𝐹‘𝐴)) |
| 42 | | 0xr 11308 |
. . . . . 6
⊢ 0 ∈
ℝ* |
| 43 | | eliccxr 13475 |
. . . . . . 7
⊢ ((𝐹‘𝐴) ∈ (0[,]+∞) → (𝐹‘𝐴) ∈
ℝ*) |
| 44 | 38, 43 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (𝐹‘𝐴) ∈
ℝ*) |
| 45 | | xrleloe 13186 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → (0 ≤
(𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))) |
| 46 | 42, 44, 45 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (0 ≤ (𝐹‘𝐴) ↔ (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴)))) |
| 47 | 41, 46 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (0 < (𝐹‘𝐴) ∨ 0 = (𝐹‘𝐴))) |
| 48 | 47 | ord 865 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (¬ 0 < (𝐹‘𝐴) → 0 = (𝐹‘𝐴))) |
| 49 | 35, 48 | mt3d 148 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 0 < (𝐹‘𝐴)) |
| 50 | | 1xr 11320 |
. . . . 5
⊢ 1 ∈
ℝ* |
| 51 | | ifcl 4571 |
. . . . 5
⊢ ((1
∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → if(1
≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈
ℝ*) |
| 52 | 50, 44, 51 | sylancr 587 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈
ℝ*) |
| 53 | | 1red 11262 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 1 ∈ ℝ) |
| 54 | | 0lt1 11785 |
. . . . . 6
⊢ 0 <
1 |
| 55 | | breq2 5147 |
. . . . . . 7
⊢ (1 = if(1
≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) → (0 < 1 ↔ 0 < if(1 ≤
(𝐹‘𝐴), 1, (𝐹‘𝐴)))) |
| 56 | | breq2 5147 |
. . . . . . 7
⊢ ((𝐹‘𝐴) = if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) → (0 < (𝐹‘𝐴) ↔ 0 < if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)))) |
| 57 | 55, 56 | ifboth 4565 |
. . . . . 6
⊢ ((0 <
1 ∧ 0 < (𝐹‘𝐴)) → 0 < if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴))) |
| 58 | 54, 49, 57 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 0 < if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴))) |
| 59 | | xrltle 13191 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈ ℝ*) → (0
< if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) → 0 ≤ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)))) |
| 60 | 42, 52, 59 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (0 < if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) → 0 ≤ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)))) |
| 61 | 58, 60 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → 0 ≤ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴))) |
| 62 | | xrmin1 13219 |
. . . . 5
⊢ ((1
∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → if(1
≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ≤ 1) |
| 63 | 50, 44, 62 | sylancr 587 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ≤ 1) |
| 64 | | xrrege0 13216 |
. . . 4
⊢ (((if(1
≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈ ℝ* ∧ 1 ∈
ℝ) ∧ (0 ≤ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∧ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ≤ 1)) → if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈ ℝ) |
| 65 | 52, 53, 61, 63, 64 | syl22anc 839 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈ ℝ) |
| 66 | 65, 58 | elrpd 13074 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈
ℝ+) |
| 67 | 49, 66 | jca 511 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (0 < (𝐹‘𝐴) ∧ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈
ℝ+)) |