Description: Predecessor class is unaffected by restriction to the base class. (Contributed by Scott Fenton, 25-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | predres | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrab2 | |
|
2 | sseqin2 | |
|
3 | 1 2 | mpbi | |
4 | dfrab2 | |
|
5 | 3 4 | eqtr2i | |
6 | iniseg | |
|
7 | 6 | ineq2d | |
8 | incom | |
|
9 | 7 8 | eqtrdi | |
10 | iniseg | |
|
11 | brres | |
|
12 | 11 | abbidv | |
13 | df-rab | |
|
14 | 12 13 | eqtr4di | |
15 | 10 14 | eqtrd | |
16 | 15 | ineq2d | |
17 | 5 9 16 | 3eqtr4a | |
18 | df-pred | |
|
19 | df-pred | |
|
20 | 17 18 19 | 3eqtr4g | |
21 | predprc | |
|
22 | predprc | |
|
23 | 21 22 | eqtr4d | |
24 | 20 23 | pm2.61i | |