Theorem predfrirr

Description: Given a well-founded relation, a class is not a member of its predecessor class. (Contributed by Scott Fenton, 22-Apr-2011)

	Ref	Expression
Assertion	predfrirr	|- ( R Fr A -> -. X e. Pred ( R , A , X ) )

Proof

Step	Hyp	Ref	Expression
1		frirr	|- ( ( R Fr A /\ X e. A ) -> -. X R X )
2		elpredg	|- ( ( X e. A /\ X e. A ) -> ( X e. Pred ( R , A , X ) <-> X R X ) )
3	2	anidms	|- ( X e. A -> ( X e. Pred ( R , A , X ) <-> X R X ) )
4	3	notbid	|- ( X e. A -> ( -. X e. Pred ( R , A , X ) <-> -. X R X ) )
5	1 4	syl5ibr	|- ( X e. A -> ( ( R Fr A /\ X e. A ) -> -. X e. Pred ( R , A , X ) ) )
6	5	expd	|- ( X e. A -> ( R Fr A -> ( X e. A -> -. X e. Pred ( R , A , X ) ) ) )
7	6	pm2.43b	|- ( R Fr A -> ( X e. A -> -. X e. Pred ( R , A , X ) ) )
8		predel	|- ( X e. Pred ( R , A , X ) -> X e. A )
9	8	con3i	|- ( -. X e. A -> -. X e. Pred ( R , A , X ) )
10	7 9	pm2.61d1	|- ( R Fr A -> -. X e. Pred ( R , A , X ) )