Metamath Proof Explorer

Theorem preddowncl

Description: A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011)

Ref Expression
Assertion preddowncl 
|- ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) -> ( X e. B -> Pred ( R , B , X ) = Pred ( R , A , X ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( y = X -> ( y e. B <-> X e. B ) )
2 predeq3 
 |-  ( y = X -> Pred ( R , B , y ) = Pred ( R , B , X ) )
3 predeq3 
 |-  ( y = X -> Pred ( R , A , y ) = Pred ( R , A , X ) )
4 2 3 eqeq12d 
 |-  ( y = X -> ( Pred ( R , B , y ) = Pred ( R , A , y ) <-> Pred ( R , B , X ) = Pred ( R , A , X ) ) )
5 1 4 imbi12d 
 |-  ( y = X -> ( ( y e. B -> Pred ( R , B , y ) = Pred ( R , A , y ) ) <-> ( X e. B -> Pred ( R , B , X ) = Pred ( R , A , X ) ) ) )
6 5 imbi2d 
 |-  ( y = X -> ( ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) -> ( y e. B -> Pred ( R , B , y ) = Pred ( R , A , y ) ) ) <-> ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) -> ( X e. B -> Pred ( R , B , X ) = Pred ( R , A , X ) ) ) ) )
7 predpredss 
 |-  ( B C_ A -> Pred ( R , B , y ) C_ Pred ( R , A , y ) )
8 7 ad2antrr 
 |-  ( ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) /\ y e. B ) -> Pred ( R , B , y ) C_ Pred ( R , A , y ) )
9 predeq3 
 |-  ( x = y -> Pred ( R , A , x ) = Pred ( R , A , y ) )
10 9 sseq1d 
 |-  ( x = y -> ( Pred ( R , A , x ) C_ B <-> Pred ( R , A , y ) C_ B ) )
11 10 rspccva 
 |-  ( ( A. x e. B Pred ( R , A , x ) C_ B /\ y e. B ) -> Pred ( R , A , y ) C_ B )
12 11 sseld 
 |-  ( ( A. x e. B Pred ( R , A , x ) C_ B /\ y e. B ) -> ( z e. Pred ( R , A , y ) -> z e. B ) )
13 vex 
 |-  y e. _V
14 13 elpredim 
 |-  ( z e. Pred ( R , A , y ) -> z R y )
15 12 14 jca2 
 |-  ( ( A. x e. B Pred ( R , A , x ) C_ B /\ y e. B ) -> ( z e. Pred ( R , A , y ) -> ( z e. B /\ z R y ) ) )
16 vex 
 |-  z e. _V
17 16 elpred 
 |-  ( y e. B -> ( z e. Pred ( R , B , y ) <-> ( z e. B /\ z R y ) ) )
18 17 imbi2d 
 |-  ( y e. B -> ( ( z e. Pred ( R , A , y ) -> z e. Pred ( R , B , y ) ) <-> ( z e. Pred ( R , A , y ) -> ( z e. B /\ z R y ) ) ) )
19 18 adantl 
 |-  ( ( A. x e. B Pred ( R , A , x ) C_ B /\ y e. B ) -> ( ( z e. Pred ( R , A , y ) -> z e. Pred ( R , B , y ) ) <-> ( z e. Pred ( R , A , y ) -> ( z e. B /\ z R y ) ) ) )
20 15 19 mpbird 
 |-  ( ( A. x e. B Pred ( R , A , x ) C_ B /\ y e. B ) -> ( z e. Pred ( R , A , y ) -> z e. Pred ( R , B , y ) ) )
21 20 ssrdv 
 |-  ( ( A. x e. B Pred ( R , A , x ) C_ B /\ y e. B ) -> Pred ( R , A , y ) C_ Pred ( R , B , y ) )
22 21 adantll 
 |-  ( ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) /\ y e. B ) -> Pred ( R , A , y ) C_ Pred ( R , B , y ) )
23 8 22 eqssd 
 |-  ( ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) /\ y e. B ) -> Pred ( R , B , y ) = Pred ( R , A , y ) )
24 23 ex 
 |-  ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) -> ( y e. B -> Pred ( R , B , y ) = Pred ( R , A , y ) ) )
25 6 24 vtoclg 
 |-  ( X e. B -> ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) -> ( X e. B -> Pred ( R , B , X ) = Pred ( R , A , X ) ) ) )
26 25 pm2.43b 
 |-  ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) -> ( X e. B -> Pred ( R , B , X ) = Pred ( R , A , X ) ) )