Step | Hyp | Ref
| Expression |
1 | | noel 3398 |
. . . . . 6
⊢ ¬
{𝑧 ∈ {∅} ∣
𝜑} ∈
∅ |
2 | 1 | a1i 9 |
. . . . 5
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ {𝑧 ∈ {∅} ∣ 𝜑} ∈ ∅) |
3 | | ordtriexmidlem 4478 |
. . . . . . . 8
⊢ {𝑧 ∈ {∅} ∣ 𝜑} ∈ On |
4 | | 0elon 4352 |
. . . . . . . 8
⊢ ∅
∈ On |
5 | | eleq1 2220 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ 𝑦 ↔ {𝑧 ∈ {∅} ∣ 𝜑} ∈ 𝑦)) |
6 | | eqeq1 2164 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (𝑥 = 𝑦 ↔ {𝑧 ∈ {∅} ∣ 𝜑} = 𝑦)) |
7 | | eleq2 2221 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑})) |
8 | 5, 6, 7 | 3orbi123d 1293 |
. . . . . . . . 9
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ 𝑦 ∨ {𝑧 ∈ {∅} ∣ 𝜑} = 𝑦 ∨ 𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑}))) |
9 | | eleq2 2221 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → ({𝑧 ∈ {∅} ∣ 𝜑} ∈ 𝑦 ↔ {𝑧 ∈ {∅} ∣ 𝜑} ∈ ∅)) |
10 | | eqeq2 2167 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → ({𝑧 ∈ {∅} ∣ 𝜑} = 𝑦 ↔ {𝑧 ∈ {∅} ∣ 𝜑} = ∅)) |
11 | | eleq1 2220 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → (𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑})) |
12 | 9, 10, 11 | 3orbi123d 1293 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → (({𝑧 ∈ {∅} ∣ 𝜑} ∈ 𝑦 ∨ {𝑧 ∈ {∅} ∣ 𝜑} = 𝑦 ∨ 𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑}) ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ ∅ ∨ {𝑧 ∈ {∅} ∣ 𝜑} = ∅ ∨ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑}))) |
13 | 8, 12 | rspc2v 2829 |
. . . . . . . 8
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ∈ On ∧ ∅ ∈
On) → (∀𝑥
∈ On ∀𝑦 ∈
On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ({𝑧 ∈ {∅} ∣ 𝜑} ∈ ∅ ∨ {𝑧 ∈ {∅} ∣ 𝜑} = ∅ ∨ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑}))) |
14 | 3, 4, 13 | mp2an 423 |
. . . . . . 7
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ({𝑧 ∈ {∅} ∣ 𝜑} ∈ ∅ ∨ {𝑧 ∈ {∅} ∣ 𝜑} = ∅ ∨ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑})) |
15 | | 3orass 966 |
. . . . . . 7
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ∈ ∅ ∨ {𝑧 ∈ {∅} ∣ 𝜑} = ∅ ∨ ∅ ∈
{𝑧 ∈ {∅} ∣
𝜑}) ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ ∅ ∨ ({𝑧 ∈ {∅} ∣ 𝜑} = ∅ ∨ ∅ ∈
{𝑧 ∈ {∅} ∣
𝜑}))) |
16 | 14, 15 | sylib 121 |
. . . . . 6
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ({𝑧 ∈ {∅} ∣ 𝜑} ∈ ∅ ∨ ({𝑧 ∈ {∅} ∣ 𝜑} = ∅ ∨ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑}))) |
17 | 16 | orcomd 719 |
. . . . 5
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → (({𝑧 ∈ {∅} ∣ 𝜑} = ∅ ∨ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑}) ∨ {𝑧 ∈ {∅} ∣ 𝜑} ∈ ∅)) |
18 | 2, 17 | ecased 1331 |
. . . 4
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ({𝑧 ∈ {∅} ∣ 𝜑} = ∅ ∨ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑})) |
19 | | ordtriexmidlem2 4479 |
. . . . 5
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} = ∅ → ¬ 𝜑) |
20 | | 0ex 4091 |
. . . . . . . 8
⊢ ∅
∈ V |
21 | 20 | snid 3591 |
. . . . . . 7
⊢ ∅
∈ {∅} |
22 | | biidd 171 |
. . . . . . . 8
⊢ (𝑧 = ∅ → (𝜑 ↔ 𝜑)) |
23 | 22 | elrab3 2869 |
. . . . . . 7
⊢ (∅
∈ {∅} → (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ 𝜑)) |
24 | 21, 23 | ax-mp 5 |
. . . . . 6
⊢ (∅
∈ {𝑧 ∈ {∅}
∣ 𝜑} ↔ 𝜑) |
25 | 24 | biimpi 119 |
. . . . 5
⊢ (∅
∈ {𝑧 ∈ {∅}
∣ 𝜑} → 𝜑) |
26 | 19, 25 | orim12i 749 |
. . . 4
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} = ∅ ∨ ∅ ∈
{𝑧 ∈ {∅} ∣
𝜑}) → (¬ 𝜑 ∨ 𝜑)) |
27 | 18, 26 | syl 14 |
. . 3
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → (¬ 𝜑 ∨ 𝜑)) |
28 | 27 | orcomd 719 |
. 2
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → (𝜑 ∨ ¬ 𝜑)) |
29 | | df-dc 821 |
. 2
⊢
(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
30 | 28, 29 | sylibr 133 |
1
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → DECID 𝜑) |