Metamath Proof Explorer

Theorem sspred

Description: Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011)

Ref Expression
Assertion sspred 
|- ( ( B C_ A /\ Pred ( R , A , X ) C_ B ) -> Pred ( R , A , X ) = Pred ( R , B , X ) )

Proof

Step Hyp Ref Expression
1 sseqin2 
 |-  ( B C_ A <-> ( A i^i B ) = B )
2 df-pred 
 |-  Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
3 2 sseq1i 
 |-  ( Pred ( R , A , X ) C_ B <-> ( A i^i ( `' R " { X } ) ) C_ B )
4 df-ss 
 |-  ( ( A i^i ( `' R " { X } ) ) C_ B <-> ( ( A i^i ( `' R " { X } ) ) i^i B ) = ( A i^i ( `' R " { X } ) ) )
5 in32 
 |-  ( ( A i^i ( `' R " { X } ) ) i^i B ) = ( ( A i^i B ) i^i ( `' R " { X } ) )
6 5 eqeq1i 
 |-  ( ( ( A i^i ( `' R " { X } ) ) i^i B ) = ( A i^i ( `' R " { X } ) ) <-> ( ( A i^i B ) i^i ( `' R " { X } ) ) = ( A i^i ( `' R " { X } ) ) )
7 3 4 6 3bitri 
 |-  ( Pred ( R , A , X ) C_ B <-> ( ( A i^i B ) i^i ( `' R " { X } ) ) = ( A i^i ( `' R " { X } ) ) )
8 ineq1 
 |-  ( ( A i^i B ) = B -> ( ( A i^i B ) i^i ( `' R " { X } ) ) = ( B i^i ( `' R " { X } ) ) )
9 8 eqeq1d 
 |-  ( ( A i^i B ) = B -> ( ( ( A i^i B ) i^i ( `' R " { X } ) ) = ( A i^i ( `' R " { X } ) ) <-> ( B i^i ( `' R " { X } ) ) = ( A i^i ( `' R " { X } ) ) ) )
10 9 biimpa 
 |-  ( ( ( A i^i B ) = B /\ ( ( A i^i B ) i^i ( `' R " { X } ) ) = ( A i^i ( `' R " { X } ) ) ) -> ( B i^i ( `' R " { X } ) ) = ( A i^i ( `' R " { X } ) ) )
11 df-pred 
 |-  Pred ( R , B , X ) = ( B i^i ( `' R " { X } ) )
12 10 11 2 3eqtr4g 
 |-  ( ( ( A i^i B ) = B /\ ( ( A i^i B ) i^i ( `' R " { X } ) ) = ( A i^i ( `' R " { X } ) ) ) -> Pred ( R , B , X ) = Pred ( R , A , X ) )
13 12 eqcomd 
 |-  ( ( ( A i^i B ) = B /\ ( ( A i^i B ) i^i ( `' R " { X } ) ) = ( A i^i ( `' R " { X } ) ) ) -> Pred ( R , A , X ) = Pred ( R , B , X ) )
14 1 7 13 syl2anb 
 |-  ( ( B C_ A /\ Pred ( R , A , X ) C_ B ) -> Pred ( R , A , X ) = Pred ( R , B , X ) )