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 7753

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

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

**Proof of Theorem ordsuc**
Step	Hyp	Ref	Expression
1		ordsuci 7750	. 2 ⊢ (Ord 𝐴 → Ord suc 𝐴)
2		sucidg 6397	. . . 4 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		ordelord 6336	. . . . 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 6392	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
7	6	eqcomd 2739	. . . . 5 ⊢ (¬ 𝐴 ∈ V → 𝐴 = suc 𝐴)
8		ordeq 6321	. . . . 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 1541 ∈ wcel 2113 Vcvv 3437 Ord word 6313 suc csuc 6316

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2705 ax-sep 5238 ax-nul 5248 ax-pr 5374

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2712 df-cleq 2725 df-clel 2808 df-ne 2930 df-ral 3049 df-rex 3058 df-rab 3397 df-v 3439 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-br 5096 df-opab 5158 df-tr 5203 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-ord 6317 df-on 6318 df-suc 6320

This theorem is referenced by: ordpwsuc 7754 onsucb 7756 ordsucss 7757 onpsssuc 7758 ordsucelsuc 7761 ordsucsssuc 7762 ordsucuniel 7763 ordsucun 7764 onsucuni2 7773 0elsuc 7774 nlimsucg 7781 limsssuc 7789 cofon1 8596 cofon2 8597 php4 9130 cantnflt 9573 fin23lem26 10227 hsmexlem1 10328 nosupres 27666 noetasuplem4 27695 noetainflem4 27699 scutbdaybnd2lim 27778 satfn 35471 onsuct0 36557 ordsssucim 43559 dfsucon 43680

W3C validator