This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid 
 |-  ( 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 ) )