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 )