Metamath Proof Explorer


Theorem predidm

Description: Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011)

Ref Expression
Assertion predidm PredRPredRAXX=PredRAX

Proof

Step Hyp Ref Expression
1 df-pred PredRPredRAXX=PredRAXR-1X
2 df-pred PredRAX=AR-1X
3 inidm R-1XR-1X=R-1X
4 3 ineq2i AR-1XR-1X=AR-1X
5 2 4 eqtr4i PredRAX=AR-1XR-1X
6 inass AR-1XR-1X=AR-1XR-1X
7 5 6 eqtr4i PredRAX=AR-1XR-1X
8 2 ineq1i PredRAXR-1X=AR-1XR-1X
9 7 8 eqtr4i PredRAX=PredRAXR-1X
10 1 9 eqtr4i PredRPredRAXX=PredRAX