Theorem ordsucss 7837

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 6407	. . . . 5 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴)
2		ordnbtwn 6478	. . . . . . . 8 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
3		imnan 399	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
4	2, 3	sylibr 234	. . . . . . 7 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴))
5	4	adantr 480	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴))
6		ordsuc 7832	. . . . . . 7 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
7		ordtri1 6418	. . . . . . 7 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
8	6, 7	sylanb 581	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
9	5, 8	sylibrd 259	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
10	1, 9	sylan 580	. . . 4 ⊢ (((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
11	10	exp31 419	. . 3 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))))
12	11	pm2.43b 55	. 2 ⊢ (𝐴 ∈ 𝐵 → (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)))
13	12	pm2.43b 55	1 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2105   ⊆ wss 3962  Ord word 6384  suc csuc 6387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389  df-suc 6391

This theorem is referenced by:  ordelsuc  7839  ordsucelsuc  7841  orduniorsuc  7849  tfindsg2  7882  oaordi  8582  oawordeulem  8590  omeulem2  8619  oeworde  8629  oelimcl  8636  oeeui  8638  nnaordi  8654  nnawordex  8673  oaabs2  8685  omxpenlem  9111  inf3lem5  9669  cantnflt  9709  cantnflem1d  9725  cnfcom  9737  r1ordg  9815  rankr1ag  9839  cfslb2n  10305  cfsmolem  10307  fin23lem26  10362  isf32lem3  10392  ttukeylem7  10552  indpi  10944  nolesgn2ores  27731  nogesgn1ores  27733  nosupbday  27764  nosupres  27766  nosupbnd1lem1  27767  nosupbnd2  27775  noinfbday  27779  noinfres  27781  noinfbnd1lem1  27782  noinfbnd2  27790  onsucss  43255  omabs2  43321  onsucunifi  43359  nadd1suc  43381