This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem predin

Description: Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011)

Ref Expression
Assertion predin 
|- Pred ( R , ( A i^i B ) , X ) = ( Pred ( R , A , X ) i^i Pred ( R , B , X ) )

Proof

Step Hyp Ref Expression
1 inindir 
 |-  ( ( A i^i B ) i^i ( `' R " { X } ) ) = ( ( A i^i ( `' R " { X } ) ) i^i ( B i^i ( `' R " { X } ) ) )
2 df-pred 
 |-  Pred ( R , ( A i^i B ) , X ) = ( ( A i^i B ) i^i ( `' R " { X } ) )
3 df-pred 
 |-  Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
4 df-pred 
 |-  Pred ( R , B , X ) = ( B i^i ( `' R " { X } ) )
5 3 4 ineq12i 
 |-  ( Pred ( R , A , X ) i^i Pred ( R , B , X ) ) = ( ( A i^i ( `' R " { X } ) ) i^i ( B i^i ( `' R " { X } ) ) )
6 1 2 5 3eqtr4i 
 |-  Pred ( R , ( A i^i B ) , X ) = ( Pred ( R , A , X ) i^i Pred ( R , B , X ) )