Metamath Proof Explorer

Theorem predidm

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

Ref Expression
Assertion predidm 
|- Pred ( R , Pred ( R , A , X ) , X ) = Pred ( R , A , X )

Proof

Step Hyp Ref Expression
1 df-pred 
 |-  Pred ( R , Pred ( R , A , X ) , X ) = ( Pred ( R , A , X ) i^i ( `' R " { X } ) )
2 df-pred 
 |-  Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
3 inidm 
 |-  ( ( `' R " { X } ) i^i ( `' R " { X } ) ) = ( `' R " { X } )
4 3 ineq2i 
 |-  ( A i^i ( ( `' R " { X } ) i^i ( `' R " { X } ) ) ) = ( A i^i ( `' R " { X } ) )
5 2 4 eqtr4i 
 |-  Pred ( R , A , X ) = ( A i^i ( ( `' R " { X } ) i^i ( `' R " { X } ) ) )
6 inass 
 |-  ( ( A i^i ( `' R " { X } ) ) i^i ( `' R " { X } ) ) = ( A i^i ( ( `' R " { X } ) i^i ( `' R " { X } ) ) )
7 5 6 eqtr4i 
 |-  Pred ( R , A , X ) = ( ( A i^i ( `' R " { X } ) ) i^i ( `' R " { X } ) )
8 2 ineq1i 
 |-  ( Pred ( R , A , X ) i^i ( `' R " { X } ) ) = ( ( A i^i ( `' R " { X } ) ) i^i ( `' R " { X } ) )
9 7 8 eqtr4i 
 |-  Pred ( R , A , X ) = ( Pred ( R , A , X ) i^i ( `' R " { X } ) )
10 1 9 eqtr4i 
 |-  Pred ( R , Pred ( R , A , X ) , X ) = Pred ( R , A , X )