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 PredRAX=PredRAAX

Proof

Step Hyp Ref Expression
1 ssrab2 yA|yRXA
2 sseqin2 yA|yRXAAyA|yRX=yA|yRX
3 1 2 mpbi AyA|yRX=yA|yRX
4 dfrab2 yA|yRX=y|yRXA
5 3 4 eqtr2i y|yRXA=AyA|yRX
6 iniseg XVR-1X=y|yRX
7 6 ineq2d XVAR-1X=Ay|yRX
8 incom Ay|yRX=y|yRXA
9 7 8 eqtrdi XVAR-1X=y|yRXA
10 iniseg XVRA-1X=y|yRAX
11 brres XVyRAXyAyRX
12 11 abbidv XVy|yRAX=y|yAyRX
13 df-rab yA|yRX=y|yAyRX
14 12 13 eqtr4di XVy|yRAX=yA|yRX
15 10 14 eqtrd XVRA-1X=yA|yRX
16 15 ineq2d XVARA-1X=AyA|yRX
17 5 9 16 3eqtr4a XVAR-1X=ARA-1X
18 df-pred PredRAX=AR-1X
19 df-pred PredRAAX=ARA-1X
20 17 18 19 3eqtr4g XVPredRAX=PredRAAX
21 predprc ¬XVPredRAX=
22 predprc ¬XVPredRAAX=
23 21 22 eqtr4d ¬XVPredRAX=PredRAAX
24 20 23 pm2.61i PredRAX=PredRAAX