Metamath Proof Explorer


Theorem ordn2lp

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)

Ref Expression
Assertion ordn2lp OrdA¬ABBA

Proof

Step Hyp Ref Expression
1 ordirr OrdA¬AA
2 ordtr OrdATrA
3 trel TrAABBAAA
4 2 3 syl OrdAABBAAA
5 1 4 mtod OrdA¬ABBA