Metamath Proof Explorer


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 RPoAXARSeATrPredRAX=PredRAX

Proof

Step Hyp Ref Expression
1 simp2 RPoAXARSeAXA
2 simp3 RPoAXARSeARSeA
3 predpo RPoAXAyPredRAXPredRAyPredRAX
4 3 ralrimiv RPoAXAyPredRAXPredRAyPredRAX
5 4 3adant3 RPoAXARSeAyPredRAXPredRAyPredRAX
6 ssidd RPoAXARSeAPredRAXPredRAX
7 trpredmintr XARSeAyPredRAXPredRAyPredRAXPredRAXPredRAXTrPredRAXPredRAX
8 1 2 5 6 7 syl22anc RPoAXARSeATrPredRAXPredRAX
9 setlikespec XARSeAPredRAXV
10 trpredpred PredRAXVPredRAXTrPredRAX
11 9 10 syl XARSeAPredRAXTrPredRAX
12 11 3adant1 RPoAXARSeAPredRAXTrPredRAX
13 8 12 eqssd RPoAXARSeATrPredRAX=PredRAX