Metamath Proof Explorer

Theorem brredunds

Description: Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022)

Ref Expression
Assertion brredunds 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A Redunds <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) ) )

Proof

Step Hyp Ref Expression
1 sseq12 
 |-  ( ( x = A /\ y = B ) -> ( x C_ y <-> A C_ B ) )
2 1 3adant3 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( x C_ y <-> A C_ B ) )
3 ineq12 
 |-  ( ( x = A /\ z = C ) -> ( x i^i z ) = ( A i^i C ) )
4 3 3adant2 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( x i^i z ) = ( A i^i C ) )
5 ineq12 
 |-  ( ( y = B /\ z = C ) -> ( y i^i z ) = ( B i^i C ) )
6 5 3adant1 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( y i^i z ) = ( B i^i C ) )
7 4 6 eqeq12d 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ( x i^i z ) = ( y i^i z ) <-> ( A i^i C ) = ( B i^i C ) ) )
8 2 7 anbi12d 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ( x C_ y /\ ( x i^i z ) = ( y i^i z ) ) <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) ) )
9 df-redunds 
 |-  Redunds = `' { <. <. y , z >. , x >. | ( x C_ y /\ ( x i^i z ) = ( y i^i z ) ) }
10 8 9 brcnvrabga 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A Redunds <. B , C >. <-> ( A C_ B /\ ( A i^i C ) = ( B i^i C ) ) ) )