ordsuc - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ordsuc		Structured version Visualization version GIF version

Theorem ordsuc 7754

Description: A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995.) Avoid ax-un 7678. (Revised by BTernaryTau, 6-Jan-2025.)

**Assertion**
Ref	Expression
ordsuc	⊢ (Ord 𝐴 ↔ Ord suc 𝐴)

**Proof of Theorem ordsuc**
Step	Hyp	Ref	Expression
1		ordsuci 7751	. 2 ⊢ (Ord 𝐴 → Ord suc 𝐴)
2		sucidg 6393	. . . 4 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		ordelord 6332	. . . . 5 ⊢ ((Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴) → Ord 𝐴)
4	3	ex 413	. . . 4 ⊢ (Ord suc 𝐴 → (𝐴 ∈ suc 𝐴 → Ord 𝐴))
5	2, 4	syl5com 31	. . 3 ⊢ (𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
6		sucprc 6388	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
7	6	eqcomd 2745	. . . . 5 ⊢ (¬ 𝐴 ∈ V → 𝐴 = suc 𝐴)
8		ordeq 6317	. . . . 5 ⊢ (𝐴 = suc 𝐴 → (Ord 𝐴 ↔ Ord suc 𝐴))
9	7, 8	syl 17	. . . 4 ⊢ (¬ 𝐴 ∈ V → (Ord 𝐴 ↔ Ord suc 𝐴))
10	9	biimprd 249	. . 3 ⊢ (¬ 𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
11	5, 10	pm2.61i 183	. 2 ⊢ (Ord suc 𝐴 → Ord 𝐴)
12	1, 11	impbii 210	1 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 = wceq 1547 ∈ wcel 2119 Vcvv 3431 Ord word 6309 suc csuc 6312

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-ext 2711 ax-sep 5218 ax-pr 5362

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-sb 2074 df-clab 2718 df-cleq 2731 df-clel 2814 df-ne 2935 df-ral 3054 df-rex 3064 df-rab 3392 df-v 3433 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-br 5073 df-opab 5135 df-tr 5180 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-ord 6313 df-on 6314 df-suc 6316

This theorem is referenced by: ordpwsuc 7755 onsucb 7757 ordsucss 7758 onpsssuc 7759 ordsucelsuc 7762 ordsucsssuc 7763 ordsucuniel 7764 ordsucun 7765 onsucuni2 7774 0elsuc 7775 nlimsucg 7782 limsssuc 7790 cofon1 8598 cofon2 8599 php4 9134 cantnflt 9584 fin23lem26 10238 hsmexlem1 10339 nosupres 27689 noetasuplem4 27718 noetainflem4 27722 cutbdaybnd2lim 27807 satfn 35583 onsuct0 36669 ordsssucim 43847 dfsucon 43967

W3C validator