Metamath Proof Explorer

Theorem predpo

Description: Property of the precessor class for partial orderings. (Contributed by Scott Fenton, 28-Apr-2012)

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 predel 
 |-  ( Y e. Pred ( R , A , X ) -> Y e. A )
2 elpredg 
 |-  ( ( X e. A /\ Y e. A ) -> ( Y e. Pred ( R , A , X ) <-> Y R X ) )
3 2 adantll 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. A ) -> ( Y e. Pred ( R , A , X ) <-> Y R X ) )
4 potr 
 |-  ( ( R Po A /\ ( z e. A /\ Y e. A /\ X e. A ) ) -> ( ( z R Y /\ Y R X ) -> z R X ) )
5 4 3exp2 
 |-  ( R Po A -> ( z e. A -> ( Y e. A -> ( X e. A -> ( ( z R Y /\ Y R X ) -> z R X ) ) ) ) )
6 5 com24 
 |-  ( R Po A -> ( X e. A -> ( Y e. A -> ( z e. A -> ( ( z R Y /\ Y R X ) -> z R X ) ) ) ) )
7 6 imp31 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. A ) -> ( z e. A -> ( ( z R Y /\ Y R X ) -> z R X ) ) )
8 7 com13 
 |-  ( ( z R Y /\ Y R X ) -> ( z e. A -> ( ( ( R Po A /\ X e. A ) /\ Y e. A ) -> z R X ) ) )
9 8 ex 
 |-  ( z R Y -> ( Y R X -> ( z e. A -> ( ( ( R Po A /\ X e. A ) /\ Y e. A ) -> z R X ) ) ) )
10 9 com14 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. A ) -> ( Y R X -> ( z e. A -> ( z R Y -> z R X ) ) ) )
11 3 10 sylbid 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. A ) -> ( Y e. Pred ( R , A , X ) -> ( z e. A -> ( z R Y -> z R X ) ) ) )
12 11 ex 
 |-  ( ( R Po A /\ X e. A ) -> ( Y e. A -> ( Y e. Pred ( R , A , X ) -> ( z e. A -> ( z R Y -> z R X ) ) ) ) )
13 12 com23 
 |-  ( ( R Po A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> ( Y e. A -> ( z e. A -> ( z R Y -> z R X ) ) ) ) )
14 13 3imp 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) /\ Y e. A ) -> ( z e. A -> ( z R Y -> z R X ) ) )
15 14 imdistand 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) /\ Y e. A ) -> ( ( z e. A /\ z R Y ) -> ( z e. A /\ z R X ) ) )
16 vex 
 |-  z e. _V
17 16 elpred 
 |-  ( Y e. A -> ( z e. Pred ( R , A , Y ) <-> ( z e. A /\ z R Y ) ) )
18 17 3ad2ant3 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) /\ Y e. A ) -> ( z e. Pred ( R , A , Y ) <-> ( z e. A /\ z R Y ) ) )
19 16 elpred 
 |-  ( X e. A -> ( z e. Pred ( R , A , X ) <-> ( z e. A /\ z R X ) ) )
20 19 adantl 
 |-  ( ( R Po A /\ X e. A ) -> ( z e. Pred ( R , A , X ) <-> ( z e. A /\ z R X ) ) )
21 20 3ad2ant1 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) /\ Y e. A ) -> ( z e. Pred ( R , A , X ) <-> ( z e. A /\ z R X ) ) )
22 15 18 21 3imtr4d 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) /\ Y e. A ) -> ( z e. Pred ( R , A , Y ) -> z e. Pred ( R , A , X ) ) )
23 22 ssrdv 
 |-  ( ( ( R Po A /\ X e. A ) /\ Y e. Pred ( R , A , X ) /\ Y e. A ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) )
24 23 3exp 
 |-  ( ( R Po A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> ( Y e. A -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) ) ) )
25 1 24 mpdi 
 |-  ( ( R Po A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) ) )