| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sucidg | Structured version Visualization version GIF version | ||
| Description: Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). Lemma 1.7 of [Schloeder] p. 1. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.) |
| Ref | Expression |
|---|---|
| sucidg | ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2737 | . . 3 ⊢ 𝐴 = 𝐴 | |
| 2 | 1 | olci 867 | . 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴) |
| 3 | elsucg 6452 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴))) | |
| 4 | 2, 3 | mpbiri 258 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 848 = wceq 1540 ∈ wcel 2108 suc csuc 6386 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-sn 4627 df-suc 6390 |
| This theorem is referenced by: sucid 6466 nsuceq0 6467 trsuc 6471 sucssel 6479 ordsuc 7833 ordsucOLD 7834 onpsssuc 7839 nlimsucg 7863 tfrlem11 8428 tfrlem13 8430 tz7.44-2 8447 omeulem1 8620 oeordi 8625 oeeulem 8639 dif1enlem 9196 dif1enlemOLD 9197 rexdif1en 9198 rexdif1enOLD 9199 dif1en 9200 dif1enOLD 9202 php4 9250 wofib 9585 suc11reg 9659 cantnfle 9711 cantnflt2 9713 cantnfp1lem3 9720 cantnflem1 9729 dfac12lem1 10184 dfac12lem2 10185 ttukeylem3 10551 ttukeylem7 10555 r1wunlim 10777 noresle 27742 nosupprefixmo 27745 noinfprefixmo 27746 fmla 35386 ex-sategoelelomsuc 35431 ontgval 36432 sucneqond 37366 finxpreclem4 37395 finxpsuclem 37398 onexgt 43252 onepsuc 43264 ordnexbtwnsuc 43280 nlimsuc 43454 sucomisnotcard 43557 |
| Copyright terms: Public domain | W3C validator |