Proof of Theorem exmidn0m
Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . . 5
⊢
((EXMID ∧ ∃𝑦 𝑦 ∈ 𝑥) → ∃𝑦 𝑦 ∈ 𝑥) |
2 | 1 | olcd 729 |
. . . 4
⊢
((EXMID ∧ ∃𝑦 𝑦 ∈ 𝑥) → (𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥)) |
3 | | notm0 3434 |
. . . . . . 7
⊢ (¬
∃𝑦 𝑦 ∈ 𝑥 ↔ 𝑥 = ∅) |
4 | 3 | biimpi 119 |
. . . . . 6
⊢ (¬
∃𝑦 𝑦 ∈ 𝑥 → 𝑥 = ∅) |
5 | 4 | adantl 275 |
. . . . 5
⊢
((EXMID ∧ ¬ ∃𝑦 𝑦 ∈ 𝑥) → 𝑥 = ∅) |
6 | 5 | orcd 728 |
. . . 4
⊢
((EXMID ∧ ¬ ∃𝑦 𝑦 ∈ 𝑥) → (𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥)) |
7 | | exmidexmid 4180 |
. . . . 5
⊢
(EXMID → DECID ∃𝑦 𝑦 ∈ 𝑥) |
8 | | exmiddc 831 |
. . . . 5
⊢
(DECID ∃𝑦 𝑦 ∈ 𝑥 → (∃𝑦 𝑦 ∈ 𝑥 ∨ ¬ ∃𝑦 𝑦 ∈ 𝑥)) |
9 | 7, 8 | syl 14 |
. . . 4
⊢
(EXMID → (∃𝑦 𝑦 ∈ 𝑥 ∨ ¬ ∃𝑦 𝑦 ∈ 𝑥)) |
10 | 2, 6, 9 | mpjaodan 793 |
. . 3
⊢
(EXMID → (𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥)) |
11 | 10 | alrimiv 1867 |
. 2
⊢
(EXMID → ∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥)) |
12 | | orc 707 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 = ∅ ∨ 𝑥 = {∅})) |
13 | 12 | a1d 22 |
. . . . 5
⊢ (𝑥 = ∅ → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
14 | | sssnm 3739 |
. . . . . . . 8
⊢
(∃𝑦 𝑦 ∈ 𝑥 → (𝑥 ⊆ {∅} ↔ 𝑥 = {∅})) |
15 | 14 | biimpa 294 |
. . . . . . 7
⊢
((∃𝑦 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ {∅}) → 𝑥 = {∅}) |
16 | 15 | olcd 729 |
. . . . . 6
⊢
((∃𝑦 𝑦 ∈ 𝑥 ∧ 𝑥 ⊆ {∅}) → (𝑥 = ∅ ∨ 𝑥 = {∅})) |
17 | 16 | ex 114 |
. . . . 5
⊢
(∃𝑦 𝑦 ∈ 𝑥 → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
18 | 13, 17 | jaoi 711 |
. . . 4
⊢ ((𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥) → (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
19 | 18 | alimi 1448 |
. . 3
⊢
(∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥) → ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
20 | | exmid01 4182 |
. . 3
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
21 | 19, 20 | sylibr 133 |
. 2
⊢
(∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥) →
EXMID) |
22 | 11, 21 | impbii 125 |
1
⊢
(EXMID ↔ ∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥)) |