Metamath Proof Explorer


Theorem predtrss

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 RA×ARA×ARYPredRAXXAPredRAYPredRAX

Proof

Step Hyp Ref Expression
1 simpr RA×ARA×ARYPredRAXXAzAzA
2 predel YPredRAXYA
3 2 3ad2ant2 RA×ARA×ARYPredRAXXAYA
4 3 adantr RA×ARA×ARYPredRAXXAzAYA
5 brxp zA×AYzAYA
6 1 4 5 sylanbrc RA×ARA×ARYPredRAXXAzAzA×AY
7 brin zRA×AYzRYzA×AY
8 predbrg XAYPredRAXYRX
9 8 ancoms YPredRAXXAYRX
10 9 3adant1 RA×ARA×ARYPredRAXXAYRX
11 10 adantr RA×ARA×ARYPredRAXXAzAYRX
12 simpl3 RA×ARA×ARYPredRAXXAzAXA
13 brxp YA×AXYAXA
14 4 12 13 sylanbrc RA×ARA×ARYPredRAXXAzAYA×AX
15 brin YRA×AXYRXYA×AX
16 11 14 15 sylanbrc RA×ARA×ARYPredRAXXAzAYRA×AX
17 breq2 y=YzRA×AyzRA×AY
18 breq1 y=YyRA×AXYRA×AX
19 17 18 anbi12d y=YzRA×AyyRA×AXzRA×AYYRA×AX
20 19 spcegv YPredRAXzRA×AYYRA×AXyzRA×AyyRA×AX
21 20 3ad2ant2 RA×ARA×ARYPredRAXXAzRA×AYYRA×AXyzRA×AyyRA×AX
22 21 adantr RA×ARA×ARYPredRAXXAzAzRA×AYYRA×AXyzRA×AyyRA×AX
23 vex zV
24 brcog zVXAzRA×ARA×AXyzRA×AyyRA×AX
25 23 12 24 sylancr RA×ARA×ARYPredRAXXAzAzRA×ARA×AXyzRA×AyyRA×AX
26 22 25 sylibrd RA×ARA×ARYPredRAXXAzAzRA×AYYRA×AXzRA×ARA×AX
27 simpl1 RA×ARA×ARYPredRAXXAzARA×ARA×AR
28 27 ssbrd RA×ARA×ARYPredRAXXAzAzRA×ARA×AXzRX
29 26 28 syld RA×ARA×ARYPredRAXXAzAzRA×AYYRA×AXzRX
30 16 29 mpan2d RA×ARA×ARYPredRAXXAzAzRA×AYzRX
31 7 30 syl5bir RA×ARA×ARYPredRAXXAzAzRYzA×AYzRX
32 6 31 mpan2d RA×ARA×ARYPredRAXXAzAzRYzRX
33 32 imdistanda RA×ARA×ARYPredRAXXAzAzRYzAzRX
34 23 elpred YPredRAXzPredRAYzAzRY
35 34 3ad2ant2 RA×ARA×ARYPredRAXXAzPredRAYzAzRY
36 23 elpred XAzPredRAXzAzRX
37 36 3ad2ant3 RA×ARA×ARYPredRAXXAzPredRAXzAzRX
38 33 35 37 3imtr4d RA×ARA×ARYPredRAXXAzPredRAYzPredRAX
39 38 ssrdv RA×ARA×ARYPredRAXXAPredRAYPredRAX