Proof of Theorem maxlp
| Step | Hyp | Ref
| Expression |
| 1 | | ssid 4006 |
. . . . 5
⊢ 𝑋 ⊆ 𝑋 |
| 2 | | lpfval.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
| 3 | 2 | lpss 23150 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑋) ⊆ 𝑋) |
| 4 | 1, 3 | mpan2 691 |
. . . 4
⊢ (𝐽 ∈ Top →
((limPt‘𝐽)‘𝑋) ⊆ 𝑋) |
| 5 | 4 | sseld 3982 |
. . 3
⊢ (𝐽 ∈ Top → (𝑃 ∈ ((limPt‘𝐽)‘𝑋) → 𝑃 ∈ 𝑋)) |
| 6 | 5 | pm4.71rd 562 |
. 2
⊢ (𝐽 ∈ Top → (𝑃 ∈ ((limPt‘𝐽)‘𝑋) ↔ (𝑃 ∈ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑋)))) |
| 7 | | simpl 482 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → 𝐽 ∈ Top) |
| 8 | 2 | islp 23148 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑋) ↔ 𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ {𝑃})))) |
| 9 | 7, 1, 8 | sylancl 586 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑋) ↔ 𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ {𝑃})))) |
| 10 | | snssi 4808 |
. . . . . 6
⊢ (𝑃 ∈ 𝑋 → {𝑃} ⊆ 𝑋) |
| 11 | 2 | clsdif 23061 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ {𝑃} ⊆ 𝑋) → ((cls‘𝐽)‘(𝑋 ∖ {𝑃})) = (𝑋 ∖ ((int‘𝐽)‘{𝑃}))) |
| 12 | 10, 11 | sylan2 593 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → ((cls‘𝐽)‘(𝑋 ∖ {𝑃})) = (𝑋 ∖ ((int‘𝐽)‘{𝑃}))) |
| 13 | 12 | eleq2d 2827 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘(𝑋 ∖ {𝑃})) ↔ 𝑃 ∈ (𝑋 ∖ ((int‘𝐽)‘{𝑃})))) |
| 14 | | eldif 3961 |
. . . . . . 7
⊢ (𝑃 ∈ (𝑋 ∖ ((int‘𝐽)‘{𝑃})) ↔ (𝑃 ∈ 𝑋 ∧ ¬ 𝑃 ∈ ((int‘𝐽)‘{𝑃}))) |
| 15 | 14 | baib 535 |
. . . . . 6
⊢ (𝑃 ∈ 𝑋 → (𝑃 ∈ (𝑋 ∖ ((int‘𝐽)‘{𝑃})) ↔ ¬ 𝑃 ∈ ((int‘𝐽)‘{𝑃}))) |
| 16 | 15 | adantl 481 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ (𝑋 ∖ ((int‘𝐽)‘{𝑃})) ↔ ¬ 𝑃 ∈ ((int‘𝐽)‘{𝑃}))) |
| 17 | | snssi 4808 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ((int‘𝐽)‘{𝑃}) → {𝑃} ⊆ ((int‘𝐽)‘{𝑃})) |
| 18 | 17 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ 𝑃 ∈ ((int‘𝐽)‘{𝑃})) → {𝑃} ⊆ ((int‘𝐽)‘{𝑃})) |
| 19 | 2 | ntrss2 23065 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ {𝑃} ⊆ 𝑋) → ((int‘𝐽)‘{𝑃}) ⊆ {𝑃}) |
| 20 | 10, 19 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → ((int‘𝐽)‘{𝑃}) ⊆ {𝑃}) |
| 21 | 20 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ 𝑃 ∈ ((int‘𝐽)‘{𝑃})) → ((int‘𝐽)‘{𝑃}) ⊆ {𝑃}) |
| 22 | 18, 21 | eqssd 4001 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ 𝑃 ∈ ((int‘𝐽)‘{𝑃})) → {𝑃} = ((int‘𝐽)‘{𝑃})) |
| 23 | 2 | ntropn 23057 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ {𝑃} ⊆ 𝑋) → ((int‘𝐽)‘{𝑃}) ∈ 𝐽) |
| 24 | 10, 23 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → ((int‘𝐽)‘{𝑃}) ∈ 𝐽) |
| 25 | 24 | adantr 480 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ 𝑃 ∈ ((int‘𝐽)‘{𝑃})) → ((int‘𝐽)‘{𝑃}) ∈ 𝐽) |
| 26 | 22, 25 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ 𝑃 ∈ ((int‘𝐽)‘{𝑃})) → {𝑃} ∈ 𝐽) |
| 27 | | snidg 4660 |
. . . . . . . . 9
⊢ (𝑃 ∈ 𝑋 → 𝑃 ∈ {𝑃}) |
| 28 | 27 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ {𝑃} ∈ 𝐽) → 𝑃 ∈ {𝑃}) |
| 29 | | isopn3i 23090 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ {𝑃} ∈ 𝐽) → ((int‘𝐽)‘{𝑃}) = {𝑃}) |
| 30 | 29 | adantlr 715 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ {𝑃} ∈ 𝐽) → ((int‘𝐽)‘{𝑃}) = {𝑃}) |
| 31 | 28, 30 | eleqtrrd 2844 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ {𝑃} ∈ 𝐽) → 𝑃 ∈ ((int‘𝐽)‘{𝑃})) |
| 32 | 26, 31 | impbida 801 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((int‘𝐽)‘{𝑃}) ↔ {𝑃} ∈ 𝐽)) |
| 33 | 32 | notbid 318 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (¬ 𝑃 ∈ ((int‘𝐽)‘{𝑃}) ↔ ¬ {𝑃} ∈ 𝐽)) |
| 34 | 16, 33 | bitrd 279 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ (𝑋 ∖ ((int‘𝐽)‘{𝑃})) ↔ ¬ {𝑃} ∈ 𝐽)) |
| 35 | 9, 13, 34 | 3bitrd 305 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑋) ↔ ¬ {𝑃} ∈ 𝐽)) |
| 36 | 35 | pm5.32da 579 |
. 2
⊢ (𝐽 ∈ Top → ((𝑃 ∈ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑋)) ↔ (𝑃 ∈ 𝑋 ∧ ¬ {𝑃} ∈ 𝐽))) |
| 37 | 6, 36 | bitrd 279 |
1
⊢ (𝐽 ∈ Top → (𝑃 ∈ ((limPt‘𝐽)‘𝑋) ↔ (𝑃 ∈ 𝑋 ∧ ¬ {𝑃} ∈ 𝐽))) |