Metamath Proof Explorer

Theorem predpo

Description: Property of the predecessor class for partial orders. (Contributed by Scott Fenton, 28-Apr-2012) (Proof shortened by Scott Fenton, 28-Oct-2024)

Ref Expression
Assertion predpo 
|- ( ( R Po A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) ) )

Proof

Step Hyp Ref Expression
1 dfpo2 
 |-  ( R Po A <-> ( ( R i^i ( _I |` A ) ) = (/) /\ ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R ) )
2 1 simprbi 
 |-  ( R Po A -> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R )
3 2 ad2antrr 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) ) -> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R )
4 simpr 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) ) -> Y e. Pred ( R , A , X ) )
5 simplr 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) ) -> X e. A )
6 predtrss 
 |-  ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) )
7 3 4 5 6 syl3anc 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) )
8 7 ex 
 |-  ( ( R Po A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) ) )