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

Metamath Proof Explorer

Theorem predres

Description: Predecessor class is unaffected by restriction to the base class. (Contributed by Scott Fenton, 25-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { y e. A | y R X } C_ A
2 sseqin2 
 |-  ( { y e. A | y R X } C_ A <-> ( A i^i { y e. A | y R X } ) = { y e. A | y R X } )
3 1 2 mpbi 
 |-  ( A i^i { y e. A | y R X } ) = { y e. A | y R X }
4 dfrab2 
 |-  { y e. A | y R X } = ( { y | y R X } i^i A )
5 3 4 eqtr2i 
 |-  ( { y | y R X } i^i A ) = ( A i^i { y e. A | y R X } )
6 iniseg 
 |-  ( X e. _V -> ( `' R " { X } ) = { y | y R X } )
7 6 ineq2d 
 |-  ( X e. _V -> ( A i^i ( `' R " { X } ) ) = ( A i^i { y | y R X } ) )
8 incom 
 |-  ( A i^i { y | y R X } ) = ( { y | y R X } i^i A )
9 7 8 eqtrdi 
 |-  ( X e. _V -> ( A i^i ( `' R " { X } ) ) = ( { y | y R X } i^i A ) )
10 iniseg 
 |-  ( X e. _V -> ( `' ( R |` A ) " { X } ) = { y | y ( R |` A ) X } )
11 brres 
 |-  ( X e. _V -> ( y ( R |` A ) X <-> ( y e. A /\ y R X ) ) )
12 11 abbidv 
 |-  ( X e. _V -> { y | y ( R |` A ) X } = { y | ( y e. A /\ y R X ) } )
13 df-rab 
 |-  { y e. A | y R X } = { y | ( y e. A /\ y R X ) }
14 12 13 eqtr4di 
 |-  ( X e. _V -> { y | y ( R |` A ) X } = { y e. A | y R X } )
15 10 14 eqtrd 
 |-  ( X e. _V -> ( `' ( R |` A ) " { X } ) = { y e. A | y R X } )
16 15 ineq2d 
 |-  ( X e. _V -> ( A i^i ( `' ( R |` A ) " { X } ) ) = ( A i^i { y e. A | y R X } ) )
17 5 9 16 3eqtr4a 
 |-  ( X e. _V -> ( A i^i ( `' R " { X } ) ) = ( A i^i ( `' ( R |` A ) " { X } ) ) )
18 df-pred 
 |-  Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
19 df-pred 
 |-  Pred ( ( R |` A ) , A , X ) = ( A i^i ( `' ( R |` A ) " { X } ) )
20 17 18 19 3eqtr4g 
 |-  ( X e. _V -> Pred ( R , A , X ) = Pred ( ( R |` A ) , A , X ) )
21 predprc 
 |-  ( -. X e. _V -> Pred ( R , A , X ) = (/) )
22 predprc 
 |-  ( -. X e. _V -> Pred ( ( R |` A ) , A , X ) = (/) )
23 21 22 eqtr4d 
 |-  ( -. X e. _V -> Pred ( R , A , X ) = Pred ( ( R |` A ) , A , X ) )
24 20 23 pm2.61i 
 |-  Pred ( R , A , X ) = Pred ( ( R |` A ) , A , X )