Theorem ordsucss 7769

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 6345	. . . . 5 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴)
2		ordnbtwn 6418	. . . . . . . 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 7765	. . . . . . 7 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
7		ordtri1 6356	. . . . . . 7 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
8	6, 7	sylanb 582	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
9	5, 8	sylibrd 259	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
10	1, 9	sylan 581	. . . 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 2114   ⊆ wss 3889  Ord word 6322  suc csuc 6325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327  df-suc 6329

This theorem is referenced by:  ordelsuc  7771  ordsucelsuc  7773  orduniorsuc  7781  tfindsg2  7813  oaordi  8481  oawordeulem  8489  omeulem2  8518  oeworde  8529  oelimcl  8536  oeeui  8538  nnaordi  8554  nnawordex  8573  oaabs2  8585  omxpenlem  9016  inf3lem5  9553  cantnflt  9593  cantnflem1d  9609  cnfcom  9621  r1ordg  9702  rankr1ag  9726  cfslb2n  10190  cfsmolem  10192  fin23lem26  10247  isf32lem3  10277  ttukeylem7  10437  indpi  10830  nolesgn2ores  27636  nogesgn1ores  27638  nosupbday  27669  nosupres  27671  nosupbnd1lem1  27672  nosupbnd2  27680  noinfbday  27684  noinfres  27686  noinfbnd1lem1  27687  noinfbnd2  27695  fineqvnttrclselem2  35266  onsucss  43694  omabs2  43760  onsucunifi  43798  nadd1suc  43820