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 
|- ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> z e. A )
2 predel 
 |-  ( Y e. Pred ( R , A , X ) -> Y e. A )
3 2 3ad2ant2 
 |-  ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> Y e. A )
4 3 adantr 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> Y e. A )
5 brxp 
 |-  ( z ( A X. A ) Y <-> ( z e. A /\ Y e. A ) )
6 1 4 5 sylanbrc 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> z ( A X. A ) Y )
7 brin 
 |-  ( z ( R i^i ( A X. A ) ) Y <-> ( z R Y /\ z ( A X. A ) Y ) )
8 predbrg 
 |-  ( ( X e. A /\ Y e. Pred ( R , A , X ) ) -> Y R X )
9 8 ancoms 
 |-  ( ( Y e. Pred ( R , A , X ) /\ X e. A ) -> Y R X )
10 9 3adant1 
 |-  ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> Y R X )
11 10 adantr 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> Y R X )
12 simpl3 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> X e. A )
13 brxp 
 |-  ( Y ( A X. A ) X <-> ( Y e. A /\ X e. A ) )
14 4 12 13 sylanbrc 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> Y ( A X. A ) X )
15 brin 
 |-  ( Y ( R i^i ( A X. A ) ) X <-> ( Y R X /\ Y ( A X. A ) X ) )
16 11 14 15 sylanbrc 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> Y ( R i^i ( A X. A ) ) X )
17 breq2 
 |-  ( y = Y -> ( z ( R i^i ( A X. A ) ) y <-> z ( R i^i ( A X. A ) ) Y ) )
18 breq1 
 |-  ( y = Y -> ( y ( R i^i ( A X. A ) ) X <-> Y ( R i^i ( A X. A ) ) X ) )
19 17 18 anbi12d 
 |-  ( y = Y -> ( ( z ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) X ) <-> ( z ( R i^i ( A X. A ) ) Y /\ Y ( R i^i ( A X. A ) ) X ) ) )
20 19 spcegv 
 |-  ( Y e. Pred ( R , A , X ) -> ( ( z ( R i^i ( A X. A ) ) Y /\ Y ( R i^i ( A X. A ) ) X ) -> E. y ( z ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) X ) ) )
21 20 3ad2ant2 
 |-  ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> ( ( z ( R i^i ( A X. A ) ) Y /\ Y ( R i^i ( A X. A ) ) X ) -> E. y ( z ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) X ) ) )
22 21 adantr 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> ( ( z ( R i^i ( A X. A ) ) Y /\ Y ( R i^i ( A X. A ) ) X ) -> E. y ( z ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) X ) ) )
23 vex 
 |-  z e. _V
24 brcog 
 |-  ( ( z e. _V /\ X e. A ) -> ( z ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) X <-> E. y ( z ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) X ) ) )
25 23 12 24 sylancr 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> ( z ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) X <-> E. y ( z ( R i^i ( A X. A ) ) y /\ y ( R i^i ( A X. A ) ) X ) ) )
26 22 25 sylibrd 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> ( ( z ( R i^i ( A X. A ) ) Y /\ Y ( R i^i ( A X. A ) ) X ) -> z ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) X ) )
27 simpl1 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R )
28 27 ssbrd 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> ( z ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) X -> z R X ) )
29 26 28 syld 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> ( ( z ( R i^i ( A X. A ) ) Y /\ Y ( R i^i ( A X. A ) ) X ) -> z R X ) )
30 16 29 mpan2d 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> ( z ( R i^i ( A X. A ) ) Y -> z R X ) )
31 7 30 syl5bir 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> ( ( z R Y /\ z ( A X. A ) Y ) -> z R X ) )
32 6 31 mpan2d 
 |-  ( ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) /\ z e. A ) -> ( z R Y -> z R X ) )
33 32 imdistanda 
 |-  ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> ( ( z e. A /\ z R Y ) -> ( z e. A /\ z R X ) ) )
34 23 elpred 
 |-  ( Y e. Pred ( R , A , X ) -> ( z e. Pred ( R , A , Y ) <-> ( z e. A /\ z R Y ) ) )
35 34 3ad2ant2 
 |-  ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> ( z e. Pred ( R , A , Y ) <-> ( z e. A /\ z R Y ) ) )
36 23 elpred 
 |-  ( X e. A -> ( z e. Pred ( R , A , X ) <-> ( z e. A /\ z R X ) ) )
37 36 3ad2ant3 
 |-  ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> ( z e. Pred ( R , A , X ) <-> ( z e. A /\ z R X ) ) )
38 33 35 37 3imtr4d 
 |-  ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> ( z e. Pred ( R , A , Y ) -> z e. Pred ( R , A , X ) ) )
39 38 ssrdv 
 |-  ( ( ( ( R i^i ( A X. A ) ) o. ( R i^i ( A X. A ) ) ) C_ R /\ Y e. Pred ( R , A , X ) /\ X e. A ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) )