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 \to \neg X \in Pred (R, A, X)$

Step	Hyp	Ref	Expression
1		frirr	$⊢ (R Fr A \land X \in A) \to \neg X R X$
2		elpredg	$⊢ (X \in A \land X \in A) \to (X \in Pred (R, A, X) \leftrightarrow X R X)$
3	2	anidms	$⊢ X \in A \to (X \in Pred (R, A, X) \leftrightarrow X R X)$
4	3	notbid	$⊢ X \in A \to (\neg X \in Pred (R, A, X) \leftrightarrow \neg X R X)$
5	1 4	imbitrrid	$⊢ X \in A \to ((R Fr A \land X \in A) \to \neg X \in Pred (R, A, X))$
6	5	expd	$⊢ X \in A \to (R Fr A \to (X \in A \to \neg X \in Pred (R, A, X)))$
7	6	pm2.43b	$⊢ R Fr A \to (X \in A \to \neg X \in Pred (R, A, X))$
8		predel	$⊢ X \in Pred (R, A, X) \to X \in A$
9	8	con3i	$⊢ \neg X \in A \to \neg X \in Pred (R, A, X)$
10	7 9	pm2.61d1	$⊢ R Fr A \to \neg X \in Pred (R, A, X)$

Metamath Proof Explorer