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	$$⊢\mathrm{Ord}A\to \neg \left(A\in B\wedge B\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordirr	$$⊢\mathrm{Ord}A\to \neg A\in A$$
2		ordtr	$$⊢\mathrm{Ord}A\to \mathrm{Tr}A$$
3		trel	$$⊢\mathrm{Tr}A\to \left(\left(A\in B\wedge B\in A\right)\to A\in A\right)$$
4	2 3	syl	$$⊢\mathrm{Ord}A\to \left(\left(A\in B\wedge B\in A\right)\to A\in A\right)$$
5	1 4	mtod	$$⊢\mathrm{Ord}A\to \neg \left(A\in B\wedge B\in A\right)$$