![]() |
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 4247 | . . . 4 ⊢ ¬ 𝐴 ∈ ∅ | |
2 | sucidg 6237 | . . . . 5 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) | |
3 | eleq2 2878 | . . . . 5 ⊢ (suc 𝐴 = ∅ → (𝐴 ∈ suc 𝐴 ↔ 𝐴 ∈ ∅)) | |
4 | 2, 3 | syl5ibcom 248 | . . . 4 ⊢ (𝐴 ∈ V → (suc 𝐴 = ∅ → 𝐴 ∈ ∅)) |
5 | 1, 4 | mtoi 202 | . . 3 ⊢ (𝐴 ∈ V → ¬ suc 𝐴 = ∅) |
6 | 0ex 5175 | . . . . . 6 ⊢ ∅ ∈ V | |
7 | eleq1 2877 | . . . . . 6 ⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈ V)) | |
8 | 6, 7 | mpbiri 261 | . . . . 5 ⊢ (𝐴 = ∅ → 𝐴 ∈ V) |
9 | 8 | con3i 157 | . . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 = ∅) |
10 | sucprc 6234 | . . . . 5 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴) | |
11 | 10 | eqeq1d 2800 | . . . 4 ⊢ (¬ 𝐴 ∈ V → (suc 𝐴 = ∅ ↔ 𝐴 = ∅)) |
12 | 9, 11 | mtbird 328 | . . 3 ⊢ (¬ 𝐴 ∈ V → ¬ suc 𝐴 = ∅) |
13 | 5, 12 | pm2.61i 185 | . 2 ⊢ ¬ suc 𝐴 = ∅ |
14 | 13 | neir 2990 | 1 ⊢ suc 𝐴 ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 Vcvv 3441 ∅c0 4243 suc csuc 6161 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-nul 5174 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ne 2988 df-v 3443 df-dif 3884 df-un 3886 df-nul 4244 df-sn 4526 df-suc 6165 |
This theorem is referenced by: 0elsuc 7530 peano3 7583 2on0 8096 oelim2 8204 limenpsi 8676 enp1i 8737 findcard2 8742 fseqdom 9437 dfac12lem2 9555 cfsuc 9668 cfpwsdom 9995 rankcf 10188 dfrdg2 33153 nosgnn0 33278 sltsolem1 33293 dfrdg4 33525 dfsucon 40231 ensucne0 40237 ensucne0OLD 40238 |
Copyright terms: Public domain | W3C validator |