Theorem ordsucss 7815

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 6384	. . . . 5 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴)
2		ordnbtwn 6458	. . . . . . . 8 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
3		imnan 404	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
4	2, 3	sylibr 237	. . . . . . 7 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴))
5	4	adantr 485	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴))
6		ordsuc 7811	. . . . . . 7 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
7		ordtri1 6396	. . . . . . 7 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
8	6, 7	sylanb 592	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
9	5, 8	sylibrd 262	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
10	1, 9	sylan 591	. . . 4 ⊢ (((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
11	10	exp31 424	. . 3 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))))
12	11	pm2.43b 56	. 2 ⊢ (𝐴 ∈ 𝐵 → (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)))
13	12	pm2.43b 56	1 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3906  Ord word 6361  suc csuc 6364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6365  df-on 6366  df-suc 6368

This theorem is referenced by:  ordelsuc  7817  ordsucelsuc  7819  orduniorsuc  7827  tfindsg2  7859  oaordi  8532  oawordeulem  8540  omeulem2  8569  oeworde  8580  oelimcl  8587  oeeui  8589  nnaordi  8605  nnawordex  8624  oaabs2  8636  omxpenlem  9067  inf3lem5  9602  cantnflt  9642  cantnflem1d  9658  cnfcom  9670  r1ordg  9751  rankr1ag  9775  cfslb2n  10253  cfsmolem  10255  fin23lem26  10310  isf32lem3  10340  ttukeylem7  10500  indpi  10893  nolesgn2ores  27814  nogesgn1ores  27816  nosupbday  27847  nosupres  27849  nosupbnd1lem1  27850  nosupbnd2  27858  noinfbday  27862  noinfres  27864  noinfbnd1lem1  27865  noinfbnd2  27873  fineqvnttrclselem2  35513  onsucss  43973  omabs2  44039  onsucunifi  44077  nadd1suc  44099