Theorem suceloni 7522

Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.)

Assertion

Ref	Expression
suceloni	⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)

Proof of Theorem suceloni

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		onelss 6228	. . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
2		velsn 4577	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3		eqimss 4023	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → 𝑥 ⊆ 𝐴)
4	2, 3	sylbi 219	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝐴} → 𝑥 ⊆ 𝐴)
5	4	a1i 11	. . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑥 ∈ {𝐴} → 𝑥 ⊆ 𝐴))
6	1, 5	orim12d 961	. . . . . . 7 ⊢ (𝐴 ∈ On → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}) → (𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴)))
7		df-suc 6192	. . . . . . . . 9 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
8	7	eleq2i 2904	. . . . . . . 8 ⊢ (𝑥 ∈ suc 𝐴 ↔ 𝑥 ∈ (𝐴 ∪ {𝐴}))
9		elun 4125	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∪ {𝐴}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}))
10	8, 9	bitr2i 278	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}) ↔ 𝑥 ∈ suc 𝐴)
11		oridm 901	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴) ↔ 𝑥 ⊆ 𝐴)
12	6, 10, 11	3imtr3g 297	. . . . . 6 ⊢ (𝐴 ∈ On → (𝑥 ∈ suc 𝐴 → 𝑥 ⊆ 𝐴))
13		sssucid 6263	. . . . . 6 ⊢ 𝐴 ⊆ suc 𝐴
14		sstr2 3974	. . . . . 6 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ suc 𝐴 → 𝑥 ⊆ suc 𝐴))
15	12, 13, 14	syl6mpi 67	. . . . 5 ⊢ (𝐴 ∈ On → (𝑥 ∈ suc 𝐴 → 𝑥 ⊆ suc 𝐴))
16	15	ralrimiv 3181	. . . 4 ⊢ (𝐴 ∈ On → ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
17		dftr3 5169	. . . 4 ⊢ (Tr suc 𝐴 ↔ ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
18	16, 17	sylibr 236	. . 3 ⊢ (𝐴 ∈ On → Tr suc 𝐴)
19		onss 7499	. . . . 5 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
20		snssi 4735	. . . . 5 ⊢ (𝐴 ∈ On → {𝐴} ⊆ On)
21	19, 20	unssd 4162	. . . 4 ⊢ (𝐴 ∈ On → (𝐴 ∪ {𝐴}) ⊆ On)
22	7, 21	eqsstrid 4015	. . 3 ⊢ (𝐴 ∈ On → suc 𝐴 ⊆ On)
23		ordon 7492	. . . 4 ⊢ Ord On
24		trssord 6203	. . . . 5 ⊢ ((Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On) → Ord suc 𝐴)
25	24	3exp 1115	. . . 4 ⊢ (Tr suc 𝐴 → (suc 𝐴 ⊆ On → (Ord On → Ord suc 𝐴)))
26	23, 25	mpii 46	. . 3 ⊢ (Tr suc 𝐴 → (suc 𝐴 ⊆ On → Ord suc 𝐴))
27	18, 22, 26	sylc 65	. 2 ⊢ (𝐴 ∈ On → Ord suc 𝐴)
28		sucexg 7519	. . 3 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ V)
29		elong 6194	. . 3 ⊢ (suc 𝐴 ∈ V → (suc 𝐴 ∈ On ↔ Ord suc 𝐴))
30	28, 29	syl 17	. 2 ⊢ (𝐴 ∈ On → (suc 𝐴 ∈ On ↔ Ord suc 𝐴))
31	27, 30	mpbird 259	1 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)

Syntax hints:   → wi 4   ↔ wb 208   ∨ wo 843   = wceq 1533   ∈ wcel 2110  ∀wral 3138  Vcvv 3495   ∪ cun 3934   ⊆ wss 3936  {csn 4561  Tr wtr 5165  Ord word 6185  Oncon0 6186  suc csuc 6188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-tr 5166  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-ord 6189  df-on 6190  df-suc 6192

This theorem is referenced by:  ordsuc  7523  unon  7540  onsuci  7547  ordunisuc2  7553  ordzsl  7554  onzsl  7555  tfindsg  7569  dfom2  7576  findsg  7603  tfrlem12  8019  oasuc  8143  omsuc  8145  onasuc  8147  oacl  8154  oneo  8201  omeulem1  8202  omeulem2  8203  oeordi  8207  oeworde  8213  oelim2  8215  oelimcl  8220  oeeulem  8221  oeeui  8222  oaabs2  8266  omxpenlem  8612  card2inf  9013  cantnflt  9129  cantnflem1d  9145  cnfcom  9157  r1ordg  9201  bndrank  9264  r1pw  9268  r1pwALT  9269  tcrank  9307  onssnum  9460  dfac12lem2  9564  cfsuc  9673  cfsmolem  9686  fin1a2lem1  9816  fin1a2lem2  9817  ttukeylem7  9931  alephreg  9998  gch2  10091  winainflem  10109  winalim2  10112  r1wunlim  10153  nqereu  10345  noextend  33168  noresle  33195  nosupno  33198  ontgval  33774  ontgsucval  33775  onsuctop  33776  sucneqond  34640  onsetreclem2  44801