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

Theorem ordelord 5932
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 2832 . . . . 5 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
21anbi2d 622 . . . 4 (𝑥 = 𝐵 → ((Ord 𝐴𝑥𝐴) ↔ (Ord 𝐴𝐵𝐴)))
3 ordeq 5917 . . . 4 (𝑥 = 𝐵 → (Ord 𝑥 ↔ Ord 𝐵))
42, 3imbi12d 335 . . 3 (𝑥 = 𝐵 → (((Ord 𝐴𝑥𝐴) → Ord 𝑥) ↔ ((Ord 𝐴𝐵𝐴) → Ord 𝐵)))
5 simpll 783 . . . . . . . . 9 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → Ord 𝐴)
6 3anrot 1122 . . . . . . . . . . . 12 ((𝑥𝐴𝑧𝑦𝑦𝑥) ↔ (𝑧𝑦𝑦𝑥𝑥𝐴))
7 3anass 1116 . . . . . . . . . . . 12 ((𝑥𝐴𝑧𝑦𝑦𝑥) ↔ (𝑥𝐴 ∧ (𝑧𝑦𝑦𝑥)))
86, 7bitr3i 268 . . . . . . . . . . 11 ((𝑧𝑦𝑦𝑥𝑥𝐴) ↔ (𝑥𝐴 ∧ (𝑧𝑦𝑦𝑥)))
9 ordtr 5924 . . . . . . . . . . . 12 (Ord 𝐴 → Tr 𝐴)
10 trel3 4921 . . . . . . . . . . . 12 (Tr 𝐴 → ((𝑧𝑦𝑦𝑥𝑥𝐴) → 𝑧𝐴))
119, 10syl 17 . . . . . . . . . . 11 (Ord 𝐴 → ((𝑧𝑦𝑦𝑥𝑥𝐴) → 𝑧𝐴))
128, 11syl5bir 234 . . . . . . . . . 10 (Ord 𝐴 → ((𝑥𝐴 ∧ (𝑧𝑦𝑦𝑥)) → 𝑧𝐴))
1312impl 447 . . . . . . . . 9 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → 𝑧𝐴)
14 trel 4920 . . . . . . . . . . . . 13 (Tr 𝐴 → ((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
159, 14syl 17 . . . . . . . . . . . 12 (Ord 𝐴 → ((𝑦𝑥𝑥𝐴) → 𝑦𝐴))
1615expcomd 406 . . . . . . . . . . 11 (Ord 𝐴 → (𝑥𝐴 → (𝑦𝑥𝑦𝐴)))
1716imp31 408 . . . . . . . . . 10 (((Ord 𝐴𝑥𝐴) ∧ 𝑦𝑥) → 𝑦𝐴)
1817adantrl 707 . . . . . . . . 9 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → 𝑦𝐴)
19 simplr 785 . . . . . . . . 9 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → 𝑥𝐴)
20 ordwe 5923 . . . . . . . . . 10 (Ord 𝐴 → E We 𝐴)
21 wetrep 5272 . . . . . . . . . 10 (( E We 𝐴 ∧ (𝑧𝐴𝑦𝐴𝑥𝐴)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2220, 21sylan 575 . . . . . . . . 9 ((Ord 𝐴 ∧ (𝑧𝐴𝑦𝐴𝑥𝐴)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
235, 13, 18, 19, 22syl13anc 1491 . . . . . . . 8 (((Ord 𝐴𝑥𝐴) ∧ (𝑧𝑦𝑦𝑥)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2423ex 401 . . . . . . 7 ((Ord 𝐴𝑥𝐴) → ((𝑧𝑦𝑦𝑥) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥)))
2524pm2.43d 53 . . . . . 6 ((Ord 𝐴𝑥𝐴) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2625alrimivv 2023 . . . . 5 ((Ord 𝐴𝑥𝐴) → ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
27 dftr2 4915 . . . . 5 (Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2826, 27sylibr 225 . . . 4 ((Ord 𝐴𝑥𝐴) → Tr 𝑥)
29 trss 4922 . . . . . . 7 (Tr 𝐴 → (𝑥𝐴𝑥𝐴))
309, 29syl 17 . . . . . 6 (Ord 𝐴 → (𝑥𝐴𝑥𝐴))
31 wess 5266 . . . . . 6 (𝑥𝐴 → ( E We 𝐴 → E We 𝑥))
3230, 20, 31syl6ci 71 . . . . 5 (Ord 𝐴 → (𝑥𝐴 → E We 𝑥))
3332imp 395 . . . 4 ((Ord 𝐴𝑥𝐴) → E We 𝑥)
34 df-ord 5913 . . . 4 (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
3528, 33, 34sylanbrc 578 . . 3 ((Ord 𝐴𝑥𝐴) → Ord 𝑥)
364, 35vtoclg 3418 . 2 (𝐵𝐴 → ((Ord 𝐴𝐵𝐴) → Ord 𝐵))
3736anabsi7 661 1 ((Ord 𝐴𝐵𝐴) → Ord 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107  wal 1650   = wceq 1652  wcel 2155  wss 3734  Tr wtr 4913   E cep 5191   We wwe 5237  Ord word 5909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-opab 4874  df-tr 4914  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-ord 5913
This theorem is referenced by:  tron  5933  ordelon  5934  ordtr2  5954  ordintdif  5959  ordsuc  7214  ordsucss  7218  ordsucelsuc  7222  ordsucuniel  7224  limsssuc  7250  smores  7655  smo11  7667  smoord  7668  smoword  7669  smogt  7670  smorndom  7671  rdglim2  7734  oesuclem  7812  ordtypelem3  8634  r1val1  8866  rankr1ag  8882  fin23lem24  9399  onsuct0  32882  dford3  38275  ordpss  39330
  Copyright terms: Public domain W3C validator