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 7788

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

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

**Proof of Theorem ordsuc**
Step	Hyp	Ref	Expression
1		ordsuci 7784	. 2 ⊢ (Ord 𝐴 → Ord suc 𝐴)
2		sucidg 6415	. . . 4 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		ordelord 6354	. . . . 5 ⊢ ((Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴) → Ord 𝐴)
4	3	ex 412	. . . 4 ⊢ (Ord suc 𝐴 → (𝐴 ∈ suc 𝐴 → Ord 𝐴))
5	2, 4	syl5com 31	. . 3 ⊢ (𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
6		sucprc 6410	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
7	6	eqcomd 2735	. . . . 5 ⊢ (¬ 𝐴 ∈ V → 𝐴 = suc 𝐴)
8		ordeq 6339	. . . . 5 ⊢ (𝐴 = suc 𝐴 → (Ord 𝐴 ↔ Ord suc 𝐴))
9	7, 8	syl 17	. . . 4 ⊢ (¬ 𝐴 ∈ V → (Ord 𝐴 ↔ Ord suc 𝐴))
10	9	biimprd 248	. . 3 ⊢ (¬ 𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
11	5, 10	pm2.61i 182	. 2 ⊢ (Ord suc 𝐴 → Ord 𝐴)
12	1, 11	impbii 209	1 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2109 Vcvv 3447 Ord word 6331 suc csuc 6334

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 2008 ax-8 2111 ax-9 2119 ax-ext 2701 ax-sep 5251 ax-nul 5261 ax-pr 5387

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3406 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-br 5108 df-opab 5170 df-tr 5215 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-ord 6335 df-on 6336 df-suc 6338

This theorem is referenced by: ordpwsuc 7790 onsucb 7792 ordsucss 7793 onpsssuc 7794 ordsucelsuc 7797 ordsucsssuc 7798 ordsucuniel 7799 ordsucun 7800 onsucuni2 7809 0elsuc 7810 nlimsucg 7818 limsssuc 7826 cofon1 8636 cofon2 8637 php4 9174 cantnflt 9625 fin23lem26 10278 hsmexlem1 10379 nosupres 27619 noetasuplem4 27648 noetainflem4 27652 scutbdaybnd2lim 27729 satfn 35342 onsuct0 36429 ordsssucim 43391 dfsucon 43512

W3C validator