MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordsucelsuc Structured version   Visualization version   GIF version

Theorem ordsucelsuc 7803
Description: Membership is inherited by successors. Generalization of Exercise 9 of [TakeutiZaring] p. 42. (Contributed by NM, 22-Jun-1998.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
Assertion
Ref Expression
ordsucelsuc (Ord 𝐵 → (𝐴𝐵 ↔ suc 𝐴 ∈ suc 𝐵))

Proof of Theorem ordsucelsuc
StepHypRef Expression
1 simpl 482 . . 3 ((Ord 𝐵𝐴𝐵) → Ord 𝐵)
2 ordelord 6376 . . 3 ((Ord 𝐵𝐴𝐵) → Ord 𝐴)
31, 2jca 511 . 2 ((Ord 𝐵𝐴𝐵) → (Ord 𝐵 ∧ Ord 𝐴))
4 simpl 482 . . 3 ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐵)
5 ordsuc 7794 . . . 4 (Ord 𝐵 ↔ Ord suc 𝐵)
6 ordelord 6376 . . . . 5 ((Ord suc 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord suc 𝐴)
7 ordsuc 7794 . . . . 5 (Ord 𝐴 ↔ Ord suc 𝐴)
86, 7sylibr 233 . . . 4 ((Ord suc 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐴)
95, 8sylanb 580 . . 3 ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → Ord 𝐴)
104, 9jca 511 . 2 ((Ord 𝐵 ∧ suc 𝐴 ∈ suc 𝐵) → (Ord 𝐵 ∧ Ord 𝐴))
11 ordsseleq 6383 . . . . . . . 8 ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴𝐵 ↔ (suc 𝐴𝐵 ∨ suc 𝐴 = 𝐵)))
127, 11sylanb 580 . . . . . . 7 ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴𝐵 ↔ (suc 𝐴𝐵 ∨ suc 𝐴 = 𝐵)))
1312ancoms 458 . . . . . 6 ((Ord 𝐵 ∧ Ord 𝐴) → (suc 𝐴𝐵 ↔ (suc 𝐴𝐵 ∨ suc 𝐴 = 𝐵)))
1413adantl 481 . . . . 5 ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴𝐵 ↔ (suc 𝐴𝐵 ∨ suc 𝐴 = 𝐵)))
15 ordsucss 7799 . . . . . . 7 (Ord 𝐵 → (𝐴𝐵 → suc 𝐴𝐵))
1615ad2antrl 725 . . . . . 6 ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴𝐵 → suc 𝐴𝐵))
17 sucssel 6449 . . . . . . 7 (𝐴 ∈ V → (suc 𝐴𝐵𝐴𝐵))
1817adantr 480 . . . . . 6 ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴𝐵𝐴𝐵))
1916, 18impbid 211 . . . . 5 ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴𝐵 ↔ suc 𝐴𝐵))
20 sucexb 7785 . . . . . . 7 (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
21 elsucg 6422 . . . . . . 7 (suc 𝐴 ∈ V → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴𝐵 ∨ suc 𝐴 = 𝐵)))
2220, 21sylbi 216 . . . . . 6 (𝐴 ∈ V → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴𝐵 ∨ suc 𝐴 = 𝐵)))
2322adantr 480 . . . . 5 ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (suc 𝐴 ∈ suc 𝐵 ↔ (suc 𝐴𝐵 ∨ suc 𝐴 = 𝐵)))
2414, 19, 233bitr4d 311 . . . 4 ((𝐴 ∈ V ∧ (Ord 𝐵 ∧ Ord 𝐴)) → (𝐴𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
2524ex 412 . . 3 (𝐴 ∈ V → ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴𝐵 ↔ suc 𝐴 ∈ suc 𝐵)))
26 elex 3485 . . . . 5 (𝐴𝐵𝐴 ∈ V)
27 elex 3485 . . . . . 6 (suc 𝐴 ∈ suc 𝐵 → suc 𝐴 ∈ V)
2827, 20sylibr 233 . . . . 5 (suc 𝐴 ∈ suc 𝐵𝐴 ∈ V)
2926, 28pm5.21ni 377 . . . 4 𝐴 ∈ V → (𝐴𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
3029a1d 25 . . 3 𝐴 ∈ V → ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴𝐵 ↔ suc 𝐴 ∈ suc 𝐵)))
3125, 30pm2.61i 182 . 2 ((Ord 𝐵 ∧ Ord 𝐴) → (𝐴𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
323, 10, 31pm5.21nd 799 1 (Ord 𝐵 → (𝐴𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844   = wceq 1533  wcel 2098  Vcvv 3466  wss 3940  Ord word 6353  suc csuc 6356
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-tr 5256  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-ord 6357  df-on 6358  df-suc 6360
This theorem is referenced by:  ordsucsssuc  7804  omsucelsucb  8453  oalimcl  8555  omlimcl  8573  pssnn  9164  pssnnOLD  9261  cantnflt  9663  cantnfp1lem3  9671  ttrcltr  9707  ttrclss  9711  ttrclselem2  9717  r1pw  9836  r1pwALT  9837  rankelpr  9864  rankelop  9865  rankxplim3  9872  infpssrlem4  10297  axdc3lem2  10442  axdc3lem4  10444  grur1a  10810  nosupno  27552  noinfno  27567  bnj570  34405  bnj1001  34459
  Copyright terms: Public domain W3C validator