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	⊢ ( 𝑅 Fr 𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		frirr	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ¬ 𝑋 𝑅 𝑋 )
2		elpredg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑋 𝑅 𝑋 ) )
3	2	anidms	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑋 𝑅 𝑋 ) )
4	3	notbid	⊢ ( 𝑋 ∈ 𝐴 → ( ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ¬ 𝑋 𝑅 𝑋 ) )
5	1 4	imbitrrid	⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝑅 Fr 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
6	5	expd	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑅 Fr 𝐴 → ( 𝑋 ∈ 𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
7	6	pm2.43b	⊢ ( 𝑅 Fr 𝐴 → ( 𝑋 ∈ 𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
8		predel	⊢ ( 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑋 ∈ 𝐴 )
9	8	con3i	⊢ ( ¬ 𝑋 ∈ 𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) )
10	7 9	pm2.61d1	⊢ ( 𝑅 Fr 𝐴 → ¬ 𝑋 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) )