Step | Hyp | Ref
| Expression |
1 | | ordtri2or2exmidlem 4508 |
. . . . 5
⊢ {𝑧 ∈ {∅, {∅}}
∣ 𝜑} ∈
On |
2 | | suc0 4394 |
. . . . . 6
⊢ suc
∅ = {∅} |
3 | | 0elon 4375 |
. . . . . . 7
⊢ ∅
∈ On |
4 | 3 | onsuci 4498 |
. . . . . 6
⊢ suc
∅ ∈ On |
5 | 2, 4 | eqeltrri 2244 |
. . . . 5
⊢ {∅}
∈ On |
6 | | sseq1 3170 |
. . . . . . 7
⊢ (𝑥 = {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → (𝑥 ⊆ 𝑦 ↔ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ 𝑦)) |
7 | | sseq2 3171 |
. . . . . . 7
⊢ (𝑥 = {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑})) |
8 | 6, 7 | orbi12d 788 |
. . . . . 6
⊢ (𝑥 = {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → ((𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) ↔ ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ 𝑦 ∨ 𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}))) |
9 | | sseq2 3171 |
. . . . . . 7
⊢ (𝑦 = {∅} → ({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ 𝑦 ↔ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆
{∅})) |
10 | | sseq1 3170 |
. . . . . . 7
⊢ (𝑦 = {∅} → (𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ {∅} ⊆ {𝑧 ∈ {∅, {∅}}
∣ 𝜑})) |
11 | 9, 10 | orbi12d 788 |
. . . . . 6
⊢ (𝑦 = {∅} → (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ 𝑦 ∨ 𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}) ↔ ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∨ {∅}
⊆ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑}))) |
12 | 8, 11 | rspc2va 2848 |
. . . . 5
⊢ ((({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ∈ On ∧
{∅} ∈ On) ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥)) → ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∨ {∅}
⊆ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑})) |
13 | 1, 5, 12 | mpanl12 434 |
. . . 4
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∨ {∅}
⊆ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑})) |
14 | 5 | onirri 4525 |
. . . . . 6
⊢ ¬
{∅} ∈ {∅} |
15 | | simpl 108 |
. . . . . . . 8
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∧ 𝜑) → {𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆
{∅}) |
16 | | simpr 109 |
. . . . . . . . 9
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∧ 𝜑) → 𝜑) |
17 | | p0ex 4172 |
. . . . . . . . . . 11
⊢ {∅}
∈ V |
18 | 17 | prid2 3688 |
. . . . . . . . . 10
⊢ {∅}
∈ {∅, {∅}} |
19 | | biidd 171 |
. . . . . . . . . . 11
⊢ (𝑧 = {∅} → (𝜑 ↔ 𝜑)) |
20 | 19 | elrab3 2887 |
. . . . . . . . . 10
⊢
({∅} ∈ {∅, {∅}} → ({∅} ∈ {𝑧 ∈ {∅, {∅}}
∣ 𝜑} ↔ 𝜑)) |
21 | 18, 20 | ax-mp 5 |
. . . . . . . . 9
⊢
({∅} ∈ {𝑧
∈ {∅, {∅}} ∣ 𝜑} ↔ 𝜑) |
22 | 16, 21 | sylibr 133 |
. . . . . . . 8
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∧ 𝜑) → {∅}
∈ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑}) |
23 | 15, 22 | sseldd 3148 |
. . . . . . 7
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∧ 𝜑) → {∅}
∈ {∅}) |
24 | 23 | ex 114 |
. . . . . 6
⊢ ({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
→ (𝜑 → {∅}
∈ {∅})) |
25 | 14, 24 | mtoi 659 |
. . . . 5
⊢ ({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
→ ¬ 𝜑) |
26 | | snssg 3714 |
. . . . . . 7
⊢ (∅
∈ On → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ {∅} ⊆ {𝑧 ∈ {∅, {∅}}
∣ 𝜑})) |
27 | 3, 26 | ax-mp 5 |
. . . . . 6
⊢ (∅
∈ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑} ↔
{∅} ⊆ {𝑧 ∈
{∅, {∅}} ∣ 𝜑}) |
28 | | 0ex 4114 |
. . . . . . . 8
⊢ ∅
∈ V |
29 | 28 | prid1 3687 |
. . . . . . 7
⊢ ∅
∈ {∅, {∅}} |
30 | | biidd 171 |
. . . . . . . 8
⊢ (𝑧 = ∅ → (𝜑 ↔ 𝜑)) |
31 | 30 | elrab3 2887 |
. . . . . . 7
⊢ (∅
∈ {∅, {∅}} → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ 𝜑)) |
32 | 29, 31 | ax-mp 5 |
. . . . . 6
⊢ (∅
∈ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑} ↔
𝜑) |
33 | 27, 32 | sylbb1 136 |
. . . . 5
⊢
({∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → 𝜑) |
34 | 25, 33 | orim12i 754 |
. . . 4
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∨ {∅} ⊆ {𝑧
∈ {∅, {∅}} ∣ 𝜑}) → (¬ 𝜑 ∨ 𝜑)) |
35 | 13, 34 | syl 14 |
. . 3
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → (¬ 𝜑 ∨ 𝜑)) |
36 | 35 | orcomd 724 |
. 2
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → (𝜑 ∨ ¬ 𝜑)) |
37 | | df-dc 830 |
. 2
⊢
(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
38 | 36, 37 | sylibr 133 |
1
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → DECID 𝜑) |