Step | Hyp | Ref
| Expression |
1 | | onsucelsucexmidlem1 4213 |
. . . 4
⊢ ∅
∈ {z
∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} |
2 | | 0elon 4095 |
. . . . . 6
⊢ ∅
∈ On |
3 | | onsucelsucexmidlem 4214 |
. . . . . 6
⊢ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} ∈ On |
4 | 2, 3 | pm3.2i 257 |
. . . . 5
⊢ (∅
∈ On ∧
{z ∈
{∅, {∅}} ∣ (z = ∅
∨ φ)}
∈ On) |
5 | | onsucelsucexmid.1 |
. . . . 5
⊢ ∀x ∈ On ∀y ∈ On (x ∈ y → suc x
∈ suc y) |
6 | | eleq1 2097 |
. . . . . . 7
⊢ (x = ∅ → (x ∈ y ↔ ∅ ∈
y)) |
7 | | suceq 4105 |
. . . . . . . 8
⊢ (x = ∅ → suc x = suc ∅) |
8 | 7 | eleq1d 2103 |
. . . . . . 7
⊢ (x = ∅ → (suc x ∈ suc y ↔ suc ∅ ∈ suc y)) |
9 | 6, 8 | imbi12d 223 |
. . . . . 6
⊢ (x = ∅ → ((x ∈ y → suc x
∈ suc y)
↔ (∅ ∈ y → suc ∅ ∈ suc y))) |
10 | | eleq2 2098 |
. . . . . . 7
⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → (∅ ∈ y ↔
∅ ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)})) |
11 | | suceq 4105 |
. . . . . . . 8
⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc y = suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}) |
12 | 11 | eleq2d 2104 |
. . . . . . 7
⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → (suc ∅ ∈ suc y ↔
suc ∅ ∈ suc {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)})) |
13 | 10, 12 | imbi12d 223 |
. . . . . 6
⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ((∅ ∈ y → suc
∅ ∈ suc y) ↔ (∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}))) |
14 | 9, 13 | rspc2va 2657 |
. . . . 5
⊢
(((∅ ∈ On ∧ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ∈ On)
∧ ∀x ∈ On ∀y ∈ On (x ∈ y → suc x
∈ suc y))
→ (∅ ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} →
suc ∅ ∈ suc {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)})) |
15 | 4, 5, 14 | mp2an 402 |
. . . 4
⊢ (∅
∈ {z
∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}) |
16 | 1, 15 | ax-mp 7 |
. . 3
⊢ suc
∅ ∈ suc {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} |
17 | | elsuci 4106 |
. . 3
⊢ (suc
∅ ∈ suc {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} →
(suc ∅ ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} ∨ suc ∅ = {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)})) |
18 | 16, 17 | ax-mp 7 |
. 2
⊢ (suc
∅ ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} ∨ suc ∅ = {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)}) |
19 | | suc0 4114 |
. . . . . 6
⊢ suc
∅ = {∅} |
20 | | p0ex 3930 |
. . . . . . 7
⊢ {∅}
∈ V |
21 | 20 | prid2 3468 |
. . . . . 6
⊢ {∅}
∈ {∅, {∅}} |
22 | 19, 21 | eqeltri 2107 |
. . . . 5
⊢ suc
∅ ∈ {∅,
{∅}} |
23 | | eqeq1 2043 |
. . . . . . 7
⊢ (z = suc ∅ → (z = ∅ ↔ suc ∅ =
∅)) |
24 | 23 | orbi1d 704 |
. . . . . 6
⊢ (z = suc ∅ → ((z = ∅ ∨ φ) ↔ (suc ∅ = ∅ ∨ φ))) |
25 | 24 | elrab3 2693 |
. . . . 5
⊢ (suc
∅ ∈ {∅, {∅}} → (suc
∅ ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} ↔
(suc ∅ = ∅ ∨ φ))) |
26 | 22, 25 | ax-mp 7 |
. . . 4
⊢ (suc
∅ ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} ↔
(suc ∅ = ∅ ∨ φ)) |
27 | | 0ex 3875 |
. . . . . . 7
⊢ ∅
∈ V |
28 | | nsuceq0g 4121 |
. . . . . . 7
⊢ (∅
∈ V → suc ∅ ≠
∅) |
29 | 27, 28 | ax-mp 7 |
. . . . . 6
⊢ suc
∅ ≠ ∅ |
30 | | df-ne 2203 |
. . . . . 6
⊢ (suc
∅ ≠ ∅ ↔ ¬ suc ∅ = ∅) |
31 | 29, 30 | mpbi 133 |
. . . . 5
⊢ ¬
suc ∅ = ∅ |
32 | | pm2.53 640 |
. . . . 5
⊢ ((suc
∅ = ∅ ∨ φ) → (¬ suc ∅ = ∅ →
φ)) |
33 | 31, 32 | mpi 15 |
. . . 4
⊢ ((suc
∅ = ∅ ∨ φ) → φ) |
34 | 26, 33 | sylbi 114 |
. . 3
⊢ (suc
∅ ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} →
φ) |
35 | 19 | eqeq1i 2044 |
. . . . 5
⊢ (suc
∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ {∅} = {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)}) |
36 | 19 | eqeq1i 2044 |
. . . . . . . 8
⊢ (suc
∅ = ∅ ↔ {∅} = ∅) |
37 | 31, 36 | mtbi 594 |
. . . . . . 7
⊢ ¬
{∅} = ∅ |
38 | 20 | elsnc 3390 |
. . . . . . 7
⊢
({∅} ∈ {∅} ↔
{∅} = ∅) |
39 | 37, 38 | mtbir 595 |
. . . . . 6
⊢ ¬
{∅} ∈ {∅} |
40 | | eleq2 2098 |
. . . . . 6
⊢
({∅} = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ({∅} ∈ {∅} ↔ {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})) |
41 | 39, 40 | mtbii 598 |
. . . . 5
⊢
({∅} = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ¬ {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}) |
42 | 35, 41 | sylbi 114 |
. . . 4
⊢ (suc
∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ¬ {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}) |
43 | | olc 631 |
. . . . 5
⊢ (φ → ({∅} = ∅ ∨ φ)) |
44 | | eqeq1 2043 |
. . . . . . . 8
⊢ (z = {∅} → (z = ∅ ↔ {∅} =
∅)) |
45 | 44 | orbi1d 704 |
. . . . . . 7
⊢ (z = {∅} → ((z = ∅ ∨ φ) ↔ ({∅} = ∅ ∨ φ))) |
46 | 45 | elrab3 2693 |
. . . . . 6
⊢
({∅} ∈ {∅, {∅}}
→ ({∅} ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} ↔
({∅} = ∅ ∨ φ))) |
47 | 21, 46 | ax-mp 7 |
. . . . 5
⊢
({∅} ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} ↔
({∅} = ∅ ∨ φ)) |
48 | 43, 47 | sylibr 137 |
. . . 4
⊢ (φ → {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}) |
49 | 42, 48 | nsyl 558 |
. . 3
⊢ (suc
∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ¬ φ) |
50 | 34, 49 | orim12i 675 |
. 2
⊢ ((suc
∅ ∈ {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)} ∨ suc ∅ = {z ∈ {∅,
{∅}} ∣ (z = ∅ ∨ φ)})
→ (φ
∨ ¬ φ)) |
51 | 18, 50 | ax-mp 7 |
1
⊢ (φ ∨ ¬
φ) |