Step | Hyp | Ref
| Expression |
1 | | simprr 527 |
. . . . 5
⊢ ((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) →
¬ 𝐴 =
{∅}) |
2 | | simpll 524 |
. . . . . . . 8
⊢ (((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ {∅}) |
3 | | simpl 108 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) →
𝐴 ⊆
{∅}) |
4 | 3 | sselda 3147 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ {∅}) |
5 | | elsni 3599 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {∅} → 𝑥 = ∅) |
6 | 4, 5 | syl 14 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) ∧ 𝑥 ∈ 𝐴) → 𝑥 = ∅) |
7 | | simpr 109 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
8 | 6, 7 | eqeltrrd 2248 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) ∧ 𝑥 ∈ 𝐴) → ∅ ∈ 𝐴) |
9 | 8 | snssd 3723 |
. . . . . . . 8
⊢ (((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) ∧ 𝑥 ∈ 𝐴) → {∅} ⊆ 𝐴) |
10 | 2, 9 | eqssd 3164 |
. . . . . . 7
⊢ (((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) ∧ 𝑥 ∈ 𝐴) → 𝐴 = {∅}) |
11 | 10 | ex 114 |
. . . . . 6
⊢ ((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) →
(𝑥 ∈ 𝐴 → 𝐴 = {∅})) |
12 | 11 | exlimdv 1812 |
. . . . 5
⊢ ((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) →
(∃𝑥 𝑥 ∈ 𝐴 → 𝐴 = {∅})) |
13 | 1, 12 | mtod 658 |
. . . 4
⊢ ((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) →
¬ ∃𝑥 𝑥 ∈ 𝐴) |
14 | | notm0 3434 |
. . . 4
⊢ (¬
∃𝑥 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅) |
15 | 13, 14 | sylib 121 |
. . 3
⊢ ((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) →
𝐴 =
∅) |
16 | | simprl 526 |
. . 3
⊢ ((𝐴 ⊆ {∅} ∧ (¬
𝐴 = ∅ ∧ ¬
𝐴 = {∅})) →
¬ 𝐴 =
∅) |
17 | 15, 16 | pm2.65da 656 |
. 2
⊢ (𝐴 ⊆ {∅} → ¬
(¬ 𝐴 = ∅ ∧
¬ 𝐴 =
{∅})) |
18 | | ioran 747 |
. 2
⊢ (¬
(𝐴 = ∅ ∨ 𝐴 = {∅}) ↔ (¬
𝐴 = ∅ ∧ ¬
𝐴 =
{∅})) |
19 | 17, 18 | sylnibr 672 |
1
⊢ (𝐴 ⊆ {∅} → ¬
¬ (𝐴 = ∅ ∨
𝐴 =
{∅})) |