Metamath Proof Explorer


Theorem predpoirr

Description: Given a partial ordering, a class is not a member of its predecessor class. (Contributed by Scott Fenton, 17-Apr-2011)

Ref Expression
Assertion predpoirr
|- ( R Po A -> -. X e. Pred ( R , A , X ) )

Proof

Step Hyp Ref Expression
1 poirr
 |-  ( ( R Po 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 Po A /\ X e. A ) -> -. X e. Pred ( R , A , X ) ) )
6 5 expd
 |-  ( X e. A -> ( R Po A -> ( X e. A -> -. X e. Pred ( R , A , X ) ) ) )
7 6 pm2.43b
 |-  ( R Po 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 Po A -> -. X e. Pred ( R , A , X ) )