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

Theorem ordelord 5643
Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
Assertion
Ref Expression
ordelord ((Ord 𝐴𝐵𝐴) → Ord 𝐵)

Proof of Theorem ordelord
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2670 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
21anbi2d 735 . . . 4 (𝑥 = 𝐵 → ((Ord 𝐴𝑥𝐴) ↔ (Ord 𝐴𝐵𝐴)))
3 ordeq 5628 . . . 4 (𝑥 = 𝐵 → (Ord 𝑥 ↔ Ord 𝐵))
42, 3imbi12d 332 . . 3 (𝑥 = 𝐵 → (((Ord 𝐴𝑥𝐴) → Ord 𝑥) ↔ ((Ord 𝐴𝐵𝐴) → Ord 𝐵)))
5 simpll 785 . . . . . . . . 9 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → Ord 𝐴)
6 3anrot 1035 . . . . . . . . . . . 12 ((𝑥𝐴𝑧𝑦𝑦𝑥) ↔ (𝑧𝑦𝑦𝑥𝑥𝐴))
7 3anass 1034 . . . . . . . . . . . 12 ((𝑥𝐴𝑧𝑦𝑦𝑥) ↔ (𝑥𝐴 ∧ (𝑧𝑦𝑦𝑥)))
86, 7bitr3i 264 . . . . . . . . . . 11 ((𝑧𝑦𝑦𝑥𝑥𝐴) ↔ (𝑥𝐴 ∧ (𝑧𝑦𝑦𝑥)))
9 ordtr 5635 . . . . . . . . . . . 12 (Ord 𝐴 → Tr 𝐴)
10 trel3 4677 . . . . . . . . . . . 12 (Tr 𝐴 → ((𝑧𝑦𝑦𝑥𝑥𝐴) → 𝑧𝐴))
119, 10syl 17 . . . . . . . . . . 11 (Ord 𝐴 → ((𝑧𝑦𝑦𝑥𝑥𝐴) → 𝑧𝐴))
128, 11syl5bir 231 . . . . . . . . . 10 (Ord 𝐴 → ((𝑥𝐴 ∧ (𝑧𝑦𝑦𝑥)) → 𝑧𝐴))
1312impl 647 . . . . . . . . 9 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → 𝑧𝐴)
14 trel 4676 . . . . . . . . . . . . 13 (Tr 𝐴 → ((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
159, 14syl 17 . . . . . . . . . . . 12 (Ord 𝐴 → ((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
1615expcomd 452 . . . . . . . . . . 11 (Ord 𝐴 → (𝑥𝐴 → (𝑦𝑥𝑦𝐴)))
1716imp31 446 . . . . . . . . . 10 (((Ord 𝐴𝑥𝐴) ∧ 𝑦𝑥) → 𝑦𝐴)
1817adantrl 747 . . . . . . . . 9 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → 𝑦𝐴)
19 simplr 787 . . . . . . . . 9 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → 𝑥𝐴)
20 ordwe 5634 . . . . . . . . . 10 (Ord 𝐴 → E We 𝐴)
21 wetrep 5016 . . . . . . . . . 10 (( E We 𝐴 ∧ (𝑧𝐴𝑦𝐴𝑥𝐴)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2220, 21sylan 486 . . . . . . . . 9 ((Ord 𝐴 ∧ (𝑧𝐴𝑦𝐴𝑥𝐴)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
235, 13, 18, 19, 22syl13anc 1319 . . . . . . . 8 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2423ex 448 . . . . . . 7 ((Ord 𝐴𝑥𝐴) → ((𝑧𝑦𝑦𝑥) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥)))
2524pm2.43d 50 . . . . . 6 ((Ord 𝐴𝑥𝐴) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2625alrimivv 1841 . . . . 5 ((Ord 𝐴𝑥𝐴) → ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
27 dftr2 4671 . . . . 5 (Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2826, 27sylibr 222 . . . 4 ((Ord 𝐴𝑥𝐴) → Tr 𝑥)
29 trss 4678 . . . . . . 7 (Tr 𝐴 → (𝑥𝐴𝑥𝐴))
309, 29syl 17 . . . . . 6 (Ord 𝐴 → (𝑥𝐴𝑥𝐴))
31 wess 5010 . . . . . 6 (𝑥𝐴 → ( E We 𝐴 → E We 𝑥))
3230, 20, 31syl6ci 68 . . . . 5 (Ord 𝐴 → (𝑥𝐴 → E We 𝑥))
3332imp 443 . . . 4 ((Ord 𝐴𝑥𝐴) → E We 𝑥)
34 df-ord 5624 . . . 4 (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
3528, 33, 34sylanbrc 694 . . 3 ((Ord 𝐴𝑥𝐴) → Ord 𝑥)
364, 35vtoclg 3233 . 2 (𝐵𝐴 → ((Ord 𝐴𝐵𝐴) → Ord 𝐵))
3736anabsi7 855 1 ((Ord 𝐴𝐵𝐴) → Ord 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030  wal 1472   = wceq 1474  wcel 1975  wss 3534  Tr wtr 4669   E cep 4932   We wwe 4981  Ord word 5620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-sep 4698  ax-nul 4707  ax-pr 4823
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-ral 2895  df-rex 2896  df-rab 2899  df-v 3169  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-sn 4120  df-pr 4122  df-op 4126  df-uni 4362  df-br 4573  df-opab 4633  df-tr 4670  df-eprel 4934  df-po 4944  df-so 4945  df-fr 4982  df-we 4984  df-ord 5624
This theorem is referenced by:  tron  5644  ordelon  5645  ordtr2  5666  ordtr3OLD  5668  ordintdif  5672  ordsuc  6878  ordsucss  6882  ordsucelsuc  6886  ordsucuniel  6888  limsssuc  6914  smores  7308  smo11  7320  smoord  7321  smoword  7322  smogt  7323  smorndom  7324  rdglim2  7387  oesuclem  7464  ordtypelem3  8280  r1val1  8504  rankr1ag  8520  fin23lem24  8999  onsuct0  31411  dford3  36411  ordpss  37474
  Copyright terms: Public domain W3C validator