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 7661

Description: The successor of an ordinal class is ordinal. (Contributed by NM, 3-Apr-1995.)

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

**Proof of Theorem ordsuc**
Step	Hyp	Ref	Expression
1		elong 6274	. . . 4 ⊢ (𝐴 ∈ V → (𝐴 ∈ On ↔ Ord 𝐴))
2		suceloni 7659	. . . . 5 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)
3		eloni 6276	. . . . 5 ⊢ (suc 𝐴 ∈ On → Ord suc 𝐴)
4	2, 3	syl 17	. . . 4 ⊢ (𝐴 ∈ On → Ord suc 𝐴)
5	1, 4	syl6bir 253	. . 3 ⊢ (𝐴 ∈ V → (Ord 𝐴 → Ord suc 𝐴))
6		sucidg 6344	. . . 4 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
7		ordelord 6288	. . . . 5 ⊢ ((Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴) → Ord 𝐴)
8	7	ex 413	. . . 4 ⊢ (Ord suc 𝐴 → (𝐴 ∈ suc 𝐴 → Ord 𝐴))
9	6, 8	syl5com 31	. . 3 ⊢ (𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
10	5, 9	impbid 211	. 2 ⊢ (𝐴 ∈ V → (Ord 𝐴 ↔ Ord suc 𝐴))
11		sucprc 6341	. . . 4 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
12	11	eqcomd 2744	. . 3 ⊢ (¬ 𝐴 ∈ V → 𝐴 = suc 𝐴)
13		ordeq 6273	. . 3 ⊢ (𝐴 = suc 𝐴 → (Ord 𝐴 ↔ Ord suc 𝐴))
14	12, 13	syl 17	. 2 ⊢ (¬ 𝐴 ∈ V → (Ord 𝐴 ↔ Ord suc 𝐴))
15	10, 14	pm2.61i 182	1 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 205 = wceq 1539 ∈ wcel 2106 Vcvv 3432 Ord word 6265 Oncon0 6266 suc csuc 6268

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-tr 5192 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-ord 6269 df-on 6270 df-suc 6272

This theorem is referenced by: ordpwsuc 7662 sucelon 7664 ordsucss 7665 onpsssuc 7666 ordsucelsuc 7669 ordsucsssuc 7670 ordsucuniel 7671 ordsucun 7672 onsucuni2 7681 0elsuc 7682 nlimsucg 7689 limsssuc 7697 php4 8996 cantnflt 9430 fin23lem26 10081 hsmexlem1 10182 satfn 33317 nosupres 33910 noetasuplem4 33939 noetainflem4 33943 scutbdaybnd2lim 34011 onsuct0 34630 dfsucon 41130