Metamath Proof Explorer


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 Pred R A X

Proof

Step Hyp Ref Expression
1 frirr R Fr A X A ¬ X R X
2 elpredg X A X A X Pred R A X X R X
3 2 anidms X A X Pred R A X X R X
4 3 notbid X A ¬ X Pred R A X ¬ X R X
5 1 4 syl5ibr X A R Fr A X A ¬ X Pred R A X
6 5 expd X A R Fr A X A ¬ X Pred R A X
7 6 pm2.43b R Fr A X A ¬ X Pred R A X
8 predel X Pred R A X X A
9 8 con3i ¬ X A ¬ X Pred R A X
10 7 9 pm2.61d1 R Fr A ¬ X Pred R A X