Proof of Theorem opnnei
| Step | Hyp | Ref
| Expression |
| 1 | | 0opn 22910 |
. . . . 5
⊢ (𝐽 ∈ Top → ∅
∈ 𝐽) |
| 2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 = ∅) → ∅
∈ 𝐽) |
| 3 | | eleq1 2829 |
. . . . 5
⊢ (𝑆 = ∅ → (𝑆 ∈ 𝐽 ↔ ∅ ∈ 𝐽)) |
| 4 | 3 | adantl 481 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 = ∅) → (𝑆 ∈ 𝐽 ↔ ∅ ∈ 𝐽)) |
| 5 | 2, 4 | mpbird 257 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 = ∅) → 𝑆 ∈ 𝐽) |
| 6 | | rzal 4509 |
. . . 4
⊢ (𝑆 = ∅ → ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥})) |
| 7 | 6 | adantl 481 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 = ∅) → ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥})) |
| 8 | 5, 7 | 2thd 265 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 = ∅) → (𝑆 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) |
| 9 | | opnneip 23127 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑥 ∈ 𝑆) → 𝑆 ∈ ((nei‘𝐽)‘{𝑥})) |
| 10 | 9 | 3expia 1122 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → (𝑥 ∈ 𝑆 → 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) |
| 11 | 10 | ralrimiv 3145 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥})) |
| 12 | 11 | ex 412 |
. . . 4
⊢ (𝐽 ∈ Top → (𝑆 ∈ 𝐽 → ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) |
| 13 | 12 | adantr 480 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ¬ 𝑆 = ∅) → (𝑆 ∈ 𝐽 → ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) |
| 14 | | df-ne 2941 |
. . . . . 6
⊢ (𝑆 ≠ ∅ ↔ ¬ 𝑆 = ∅) |
| 15 | | r19.2z 4495 |
. . . . . . 7
⊢ ((𝑆 ≠ ∅ ∧
∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥})) → ∃𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥})) |
| 16 | 15 | ex 412 |
. . . . . 6
⊢ (𝑆 ≠ ∅ →
(∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → ∃𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) |
| 17 | 14, 16 | sylbir 235 |
. . . . 5
⊢ (¬
𝑆 = ∅ →
(∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → ∃𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) |
| 18 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 19 | 18 | neii1 23114 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ ((nei‘𝐽)‘{𝑥})) → 𝑆 ⊆ ∪ 𝐽) |
| 20 | 19 | ex 412 |
. . . . . 6
⊢ (𝐽 ∈ Top → (𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → 𝑆 ⊆ ∪ 𝐽)) |
| 21 | 20 | rexlimdvw 3160 |
. . . . 5
⊢ (𝐽 ∈ Top → (∃𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → 𝑆 ⊆ ∪ 𝐽)) |
| 22 | 17, 21 | sylan9r 508 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ ¬ 𝑆 = ∅) →
(∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → 𝑆 ⊆ ∪ 𝐽)) |
| 23 | 18 | ntrss2 23065 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ((int‘𝐽)‘𝑆) ⊆ 𝑆) |
| 24 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
∧ ∀𝑥 ∈
𝑆 {𝑥} ⊆ ((int‘𝐽)‘𝑆)) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) |
| 25 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 26 | 25 | snss 4785 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ((int‘𝐽)‘𝑆) ↔ {𝑥} ⊆ ((int‘𝐽)‘𝑆)) |
| 27 | 26 | ralbii 3093 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑆 𝑥 ∈ ((int‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝑆 {𝑥} ⊆ ((int‘𝐽)‘𝑆)) |
| 28 | | dfss3 3972 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ ((int‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝑆 𝑥 ∈ ((int‘𝐽)‘𝑆)) |
| 29 | 28 | biimpri 228 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑆 𝑥 ∈ ((int‘𝐽)‘𝑆) → 𝑆 ⊆ ((int‘𝐽)‘𝑆)) |
| 30 | 29 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
∧ ∀𝑥 ∈
𝑆 𝑥 ∈ ((int‘𝐽)‘𝑆)) → 𝑆 ⊆ ((int‘𝐽)‘𝑆)) |
| 31 | 27, 30 | sylan2br 595 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
∧ ∀𝑥 ∈
𝑆 {𝑥} ⊆ ((int‘𝐽)‘𝑆)) → 𝑆 ⊆ ((int‘𝐽)‘𝑆)) |
| 32 | 24, 31 | eqssd 4001 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
∧ ∀𝑥 ∈
𝑆 {𝑥} ⊆ ((int‘𝐽)‘𝑆)) → ((int‘𝐽)‘𝑆) = 𝑆) |
| 33 | 32 | ex 412 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ (∀𝑥 ∈
𝑆 {𝑥} ⊆ ((int‘𝐽)‘𝑆) → ((int‘𝐽)‘𝑆) = 𝑆)) |
| 34 | 25 | snss 4785 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑆 ↔ {𝑥} ⊆ 𝑆) |
| 35 | | sstr2 3990 |
. . . . . . . . . . . . . 14
⊢ ({𝑥} ⊆ 𝑆 → (𝑆 ⊆ ∪ 𝐽 → {𝑥} ⊆ ∪ 𝐽)) |
| 36 | 35 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ ∪ 𝐽
→ ({𝑥} ⊆ 𝑆 → {𝑥} ⊆ ∪ 𝐽)) |
| 37 | 36 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ ({𝑥} ⊆ 𝑆 → {𝑥} ⊆ ∪ 𝐽)) |
| 38 | 34, 37 | biimtrid 242 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ (𝑥 ∈ 𝑆 → {𝑥} ⊆ ∪ 𝐽)) |
| 39 | 38 | imp 406 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
∧ 𝑥 ∈ 𝑆) → {𝑥} ⊆ ∪ 𝐽) |
| 40 | 18 | neiint 23112 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ {𝑥} ⊆ ∪ 𝐽
∧ 𝑆 ⊆ ∪ 𝐽)
→ (𝑆 ∈
((nei‘𝐽)‘{𝑥}) ↔ {𝑥} ⊆ ((int‘𝐽)‘𝑆))) |
| 41 | 40 | 3com23 1127 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽
∧ {𝑥} ⊆ ∪ 𝐽)
→ (𝑆 ∈
((nei‘𝐽)‘{𝑥}) ↔ {𝑥} ⊆ ((int‘𝐽)‘𝑆))) |
| 42 | 41 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
∧ {𝑥} ⊆ ∪ 𝐽)
→ (𝑆 ∈
((nei‘𝐽)‘{𝑥}) ↔ {𝑥} ⊆ ((int‘𝐽)‘𝑆))) |
| 43 | 39, 42 | syldan 591 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
∧ 𝑥 ∈ 𝑆) → (𝑆 ∈ ((nei‘𝐽)‘{𝑥}) ↔ {𝑥} ⊆ ((int‘𝐽)‘𝑆))) |
| 44 | 43 | ralbidva 3176 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ (∀𝑥 ∈
𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) ↔ ∀𝑥 ∈ 𝑆 {𝑥} ⊆ ((int‘𝐽)‘𝑆))) |
| 45 | 18 | isopn3 23074 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ (𝑆 ∈ 𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆)) |
| 46 | 33, 44, 45 | 3imtr4d 294 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽)
→ (∀𝑥 ∈
𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → 𝑆 ∈ 𝐽)) |
| 47 | 46 | ex 412 |
. . . . . 6
⊢ (𝐽 ∈ Top → (𝑆 ⊆ ∪ 𝐽
→ (∀𝑥 ∈
𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → 𝑆 ∈ 𝐽))) |
| 48 | 47 | com23 86 |
. . . . 5
⊢ (𝐽 ∈ Top →
(∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → (𝑆 ⊆ ∪ 𝐽 → 𝑆 ∈ 𝐽))) |
| 49 | 48 | adantr 480 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ ¬ 𝑆 = ∅) →
(∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → (𝑆 ⊆ ∪ 𝐽 → 𝑆 ∈ 𝐽))) |
| 50 | 22, 49 | mpdd 43 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ¬ 𝑆 = ∅) →
(∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}) → 𝑆 ∈ 𝐽)) |
| 51 | 13, 50 | impbid 212 |
. 2
⊢ ((𝐽 ∈ Top ∧ ¬ 𝑆 = ∅) → (𝑆 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) |
| 52 | 8, 51 | pm2.61dan 813 |
1
⊢ (𝐽 ∈ Top → (𝑆 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) |