Theorem trpredpo

Description: If R partially orders A , then the transitive predecessors are the same as the immediate predecessors . (Contributed by Scott Fenton, 28-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Assertion	trpredpo	|- ( ( R Po A /\ X e. A /\ R Se A ) -> TrPred ( R , A , X ) = Pred ( R , A , X ) )

Proof

Step	Hyp	Ref	Expression
1		simp2	|- ( ( R Po A /\ X e. A /\ R Se A ) -> X e. A )
2		simp3	|- ( ( R Po A /\ X e. A /\ R Se A ) -> R Se A )
3		predpo	|- ( ( R Po A /\ X e. A ) -> ( y e. Pred ( R , A , X ) -> Pred ( R , A , y ) C_ Pred ( R , A , X ) ) )
4	3	ralrimiv	|- ( ( R Po A /\ X e. A ) -> A. y e. Pred ( R , A , X ) Pred ( R , A , y ) C_ Pred ( R , A , X ) )
5	4	3adant3	|- ( ( R Po A /\ X e. A /\ R Se A ) -> A. y e. Pred ( R , A , X ) Pred ( R , A , y ) C_ Pred ( R , A , X ) )
6		ssidd	|- ( ( R Po A /\ X e. A /\ R Se A ) -> Pred ( R , A , X ) C_ Pred ( R , A , X ) )
7		trpredmintr	|- ( ( ( X e. A /\ R Se A ) /\ ( A. y e. Pred ( R , A , X ) Pred ( R , A , y ) C_ Pred ( R , A , X ) /\ Pred ( R , A , X ) C_ Pred ( R , A , X ) ) ) -> TrPred ( R , A , X ) C_ Pred ( R , A , X ) )
8	1 2 5 6 7	syl22anc	|- ( ( R Po A /\ X e. A /\ R Se A ) -> TrPred ( R , A , X ) C_ Pred ( R , A , X ) )
9		setlikespec	|- ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )
10		trpredpred	|- ( Pred ( R , A , X ) e. _V -> Pred ( R , A , X ) C_ TrPred ( R , A , X ) )
11	9 10	syl	|- ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) C_ TrPred ( R , A , X ) )
12	11	3adant1	|- ( ( R Po A /\ X e. A /\ R Se A ) -> Pred ( R , A , X ) C_ TrPred ( R , A , X ) )
13	8 12	eqssd	|- ( ( R Po A /\ X e. A /\ R Se A ) -> TrPred ( R , A , X ) = Pred ( R , A , X ) )