Theorem ordsucss 7823

Description: The successor of an element of an ordinal class is a subset of it. Lemma 1.14 of [Schloeder] p. 2. (Contributed by NM, 21-Jun-1998.)

Assertion

Ref	Expression
ordsucss	⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))

Proof of Theorem ordsucss

Step	Hyp	Ref	Expression
1		ordelord 6389	. . . . 5 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴)
2		ordnbtwn 6463	. . . . . . . 8 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
3		imnan 405	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
4	2, 3	sylibr 237	. . . . . . 7 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴))
5	4	adantr 486	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴))
6		ordsuc 7819	. . . . . . 7 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
7		ordtri1 6401	. . . . . . 7 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
8	6, 7	sylanb 593	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
9	5, 8	sylibrd 262	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
10	1, 9	sylan 592	. . . 4 ⊢ (((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
11	10	exp31 425	. . 3 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))))
12	11	pm2.43b 56	. 2 ⊢ (𝐴 ∈ 𝐵 → (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)))
13	12	pm2.43b 56	1 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2146   ⊆ wss 3908  Ord word 6366  suc csuc 6369

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-tr 5224  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6370  df-on 6371  df-suc 6373

This theorem is used by:  ordelsuc  7825  ordsucelsuc  7827  orduniorsuc  7835  tfindsg2  7867  oaordi  8540  oawordeulem  8548  omeulem2  8577  oeworde  8588  oelimcl  8595  oeeui  8597  nnaordi  8613  nnawordex  8632  oaabs2  8644  omxpenlem  9076  inf3lem5  9611  cantnflt  9651  cantnflem1d  9667  cnfcom  9679  r1ordg  9760  rankr1ag  9784  cfslb2n  10270  cfsmolem  10272  fin23lem26  10327  isf32lem3  10357  ttukeylem7  10517  indpi  10910  nolesgn2ores  27873  nogesgn1ores  27875  nosupbday  27906  nosupres  27908  nosupbnd1lem1  27909  nosupbnd2  27917  noinfbday  27921  noinfres  27923  noinfbnd1lem1  27924  noinfbnd2  27932  fineqvnttrclselem2  35559  onsucss  44034  omabs2  44100  onsucunifi  44138  nadd1suc  44160