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 7739

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

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

**Proof of Theorem ordsuc**
Step	Hyp	Ref	Expression
1		ordsuci 7736	. 2 ⊢ (Ord 𝐴 → Ord suc 𝐴)
2		sucidg 6384	. . . 4 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		ordelord 6323	. . . . 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 6379	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
7	6	eqcomd 2737	. . . . 5 ⊢ (¬ 𝐴 ∈ V → 𝐴 = suc 𝐴)
8		ordeq 6308	. . . . 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 2111 Vcvv 3436 Ord word 6300 suc csuc 6303

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 2113 ax-9 2121 ax-ext 2703 ax-sep 5229 ax-nul 5239 ax-pr 5365

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 2710 df-cleq 2723 df-clel 2806 df-ne 2929 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4855 df-br 5087 df-opab 5149 df-tr 5194 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-we 5566 df-ord 6304 df-on 6305 df-suc 6307

This theorem is referenced by: ordpwsuc 7740 onsucb 7742 ordsucss 7743 onpsssuc 7744 ordsucelsuc 7747 ordsucsssuc 7748 ordsucuniel 7749 ordsucun 7750 onsucuni2 7759 0elsuc 7760 nlimsucg 7767 limsssuc 7775 cofon1 8582 cofon2 8583 php4 9114 cantnflt 9557 fin23lem26 10211 hsmexlem1 10312 nosupres 27641 noetasuplem4 27670 noetainflem4 27674 scutbdaybnd2lim 27753 satfn 35391 onsuct0 36475 ordsssucim 43435 dfsucon 43556

W3C validator