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	|- ( Ord A -> -. ( A e. B /\ B e. A ) )

Proof

Step	Hyp	Ref	Expression
1		ordirr	|- ( Ord A -> -. A e. A )
2		ordtr	|- ( Ord A -> Tr A )
3		trel	|- ( Tr A -> ( ( A e. B /\ B e. A ) -> A e. A ) )
4	2 3	syl	|- ( Ord A -> ( ( A e. B /\ B e. A ) -> A e. A ) )
5	1 4	mtod	|- ( Ord A -> -. ( A e. B /\ B e. A ) )