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

Theorem ordn2lp 5897
Description: An ordinal class cannot be an element of one of its members. Variant of first part of Theorem 2.2(vii) of [BellMachover] p. 469. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
ordn2lp (Ord 𝐴 → ¬ (𝐴𝐵𝐵𝐴))

Proof of Theorem ordn2lp
StepHypRef Expression
1 ordirr 5895 . 2 (Ord 𝐴 → ¬ 𝐴𝐴)
2 ordtr 5891 . . 3 (Ord 𝐴 → Tr 𝐴)
3 trel 4906 . . 3 (Tr 𝐴 → ((𝐴𝐵𝐵𝐴) → 𝐴𝐴))
42, 3syl 17 . 2 (Ord 𝐴 → ((𝐴𝐵𝐵𝐴) → 𝐴𝐴))
51, 4mtod 189 1 (Ord 𝐴 → ¬ (𝐴𝐵𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  wcel 2148  Tr wtr 4899  Ord word 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pr 5048
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3357  df-sbc 3594  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-tr 4900  df-eprel 5176  df-fr 5222  df-we 5224  df-ord 5880
This theorem is referenced by:  ordtri1  5910  ordnbtwn  5970  ordnbtwnOLD  5971  suc11  5985  smoord  7636  unblem1  8389  cantnfp1lem3  8762  cardprclem  9026  nosepssdm  32190  slerec  32277
  Copyright terms: Public domain W3C validator