| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nsuceq0 | Structured version Visualization version GIF version | ||
| Description: No successor is empty. (Contributed by NM, 3-Apr-1995.) |
| Ref | Expression |
|---|---|
| nsuceq0 | ⊢ suc 𝐴 ≠ ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | noel 4294 | . . . 4 ⊢ ¬ 𝐴 ∈ ∅ | |
| 2 | sucidg 6448 | . . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) | |
| 3 | eleq2 2855 | . . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅)) | |
| 4 | 2, 3 | syl5ibcom 248 | . . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅)) |
| 5 | 1, 4 | mtoi 202 | . . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅) |
| 6 | 0ex 5273 | . . . . . 6 ⊢ ∅ ∈ V | |
| 7 | eleq1 2854 | . . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V)) | |
| 8 | 6, 7 | mpbiri 261 | . . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V) |
| 9 | 8 | con3i 155 | . . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅) |
| 10 | sucprc 6443 | . . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴) | |
| 11 | 10 | eqeq1d 2768 | . . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅)) |
| 12 | 9, 11 | mtbird 328 | . . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅) |
| 13 | 5, 12 | pm2.61i 184 | . 2 ⊢ ¬ suc 𝐴 = ∅ |
| 14 | 13 | neir 2964 | 1 ⊢ suc 𝐴 ≠ ∅ |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ¬ wn 3 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 Vcvv 3458 ∅c0 4289 suc csuc 6366 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2738 ax-nul 5272 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2745 df-cleq 2758 df-clel 2841 df-ne 2962 df-v 3460 df-dif 3911 df-un 3913 df-nul 4290 df-sn 4593 df-suc 6370 |
| This theorem is used by: 0elsuc 7833 peano3OLD 7890 2on0 8470 1n0 8474 oelim2 8583 limenpsi 9142 ttrclselem2 9697 fseqdom 10021 dfac12lem2 10139 cfsuc 10251 cfpwsdom 10579 rankcf 10772 nosgnn0 27837 ltssolem1 27854 dfrdg2 36297 dfrdg4 36455 dfsucon 44281 ensucne0 44287 ensucne0OLD 44288 |
| Copyright terms: Public domain | W3C validator |