Theorem ordsucss 7536

Description: The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.)

Assertion

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

Proof of Theorem ordsucss

Step	Hyp	Ref	Expression
1		ordelord 6216	. . . . 5 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴)
2		ordnbtwn 6284	. . . . . . . 8 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
3		imnan 402	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))
4	2, 3	sylibr 236	. . . . . . 7 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴))
5	4	adantr 483	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴))
6		ordsuc 7532	. . . . . . 7 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
7		ordtri1 6227	. . . . . . 7 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
8	6, 7	sylanb 583	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴))
9	5, 8	sylibrd 261	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
10	1, 9	sylan 582	. . . 4 ⊢ (((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))
11	10	exp31 422	. . 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 208   ∧ wa 398   ∈ wcel 2113   ⊆ wss 3939  Ord word 6193  suc csuc 6196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-tr 5176  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-ord 6197  df-on 6198  df-suc 6200

This theorem is referenced by:  ordelsuc  7538  ordsucelsuc  7540  orduniorsuc  7548  tfindsg2  7579  oaordi  8175  oawordeulem  8183  omeulem2  8212  oeworde  8222  oelimcl  8229  oeeui  8231  nnaordi  8247  nnawordex  8266  oaabs2  8275  omxpenlem  8621  inf3lem5  9098  cantnflt  9138  cantnflem1d  9154  cnfcom  9166  r1ordg  9210  rankr1ag  9234  cfslb2n  9693  cfsmolem  9695  fin23lem26  9750  isf32lem3  9780  ttukeylem7  9940  indpi  10332  nolesgn2ores  33183  nosupres  33211  nosupbnd1lem1  33212  nosupbnd2  33220