Theorem ordelsuc 7801

Description: A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 29-Nov-2003.)

Assertion

Ref	Expression
ordelsuc	⊢ ((𝐴 ∈ 𝐶 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵))

Proof of Theorem ordelsuc

Step	Hyp	Ref	Expression
1		ordsucss 7799	. . 3 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
2	1	adantl 481	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
3		sucssel 6449	. . 3 ⊢ (𝐴 ∈ 𝐶 → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
4	3	adantr 480	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
5	2, 4	impbid 211	1 ⊢ ((𝐴 ∈ 𝐶 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2098   ⊆ wss 3940  Ord word 6353  suc csuc 6356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-tr 5256  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-ord 6357  df-on 6358  df-suc 6360

This theorem is referenced by:  onsucmin  7802  onsucssi  7823  tfindsg2  7844  ordgt0ge1  8488  onomeneqOLD  9225  cantnflem1  9680  ttrcltr  9707  dmttrcl  9712  r1ordg  9769  r1val1  9777  rankonidlem  9819  rankxplim3  9872  ordeldifsucon  42498  ordeldif1o  42499  oaltom  42645  omltoe  42647