Description: If R is transitive over A and Y R X , then Pred ( R , A , Y ) is a subclass of Pred ( R , A , X ) . (Contributed by Scott Fenton, 28-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | predtrss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | predel | |
|
3 | 2 | 3ad2ant2 | |
4 | 3 | adantr | |
5 | brxp | |
|
6 | 1 4 5 | sylanbrc | |
7 | brin | |
|
8 | predbrg | |
|
9 | 8 | ancoms | |
10 | 9 | 3adant1 | |
11 | 10 | adantr | |
12 | simpl3 | |
|
13 | brxp | |
|
14 | 4 12 13 | sylanbrc | |
15 | brin | |
|
16 | 11 14 15 | sylanbrc | |
17 | breq2 | |
|
18 | breq1 | |
|
19 | 17 18 | anbi12d | |
20 | 19 | spcegv | |
21 | 20 | 3ad2ant2 | |
22 | 21 | adantr | |
23 | vex | |
|
24 | brcog | |
|
25 | 23 12 24 | sylancr | |
26 | 22 25 | sylibrd | |
27 | simpl1 | |
|
28 | 27 | ssbrd | |
29 | 26 28 | syld | |
30 | 16 29 | mpan2d | |
31 | 7 30 | syl5bir | |
32 | 6 31 | mpan2d | |
33 | 32 | imdistanda | |
34 | 23 | elpred | |
35 | 34 | 3ad2ant2 | |
36 | 23 | elpred | |
37 | 36 | 3ad2ant3 | |
38 | 33 35 37 | 3imtr4d | |
39 | 38 | ssrdv | |