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 7789

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

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

**Proof of Theorem ordsuc**
Step	Hyp	Ref	Expression
1		ordsuci 7786	. 2 ⊢ (Ord 𝐴 → Ord suc 𝐴)
2		sucidg 6424	. . . 4 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		ordelord 6363	. . . . 5 ⊢ ((Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴) → Ord 𝐴)
4	3	ex 416	. . . 4 ⊢ (Ord suc 𝐴 → (𝐴 ∈ suc 𝐴 → Ord 𝐴))
5	2, 4	syl5com 31	. . 3 ⊢ (𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
6		sucprc 6419	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
7	6	eqcomd 2767	. . . . 5 ⊢ (¬ 𝐴 ∈ V → 𝐴 = suc 𝐴)
8		ordeq 6348	. . . . 5 ⊢ (𝐴 = suc 𝐴 → (Ord 𝐴 ↔ Ord suc 𝐴))
9	7, 8	syl 17	. . . 4 ⊢ (¬ 𝐴 ∈ V → (Ord 𝐴 ↔ Ord suc 𝐴))
10	9	biimprd 250	. . 3 ⊢ (¬ 𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
11	5, 10	pm2.61i 183	. 2 ⊢ (Ord suc 𝐴 → Ord 𝐴)
12	1, 11	impbii 211	1 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 = wceq 1559 ∈ wcel 2141 Vcvv 3453 Ord word 6340 suc csuc 6343

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-ext 2733 ax-sep 5243 ax-pr 5387

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-sb 2090 df-clab 2740 df-cleq 2753 df-clel 2836 df-ne 2957 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-br 5098 df-opab 5160 df-tr 5205 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-ord 6344 df-on 6345 df-suc 6347

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 7817 limsssuc 7825 cofon1 8636 cofon2 8637 php4 9172 cantnflt 9621 fin23lem26 10276 hsmexlem1 10377 nosupres 27759 noetasuplem4 27788 noetainflem4 27792 cutbdaybnd2lim 27878 satfn 35666 onsuct0 36762 ordsssucim 43940 dfsucon 44060

W3C validator