Metamath Proof Explorer

Theorem 1cosscnvxrn

Description: Cosets by the converse range Cartesian product. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

Ref Expression
Assertion 1cosscnvxrn 
|- ,~ `' ( A |X. B ) = ( ,~ `' A i^i ,~ `' B )

Proof

Step Hyp Ref Expression
1 br1cosscnvxrn 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x ,~ `' ( A |X. B ) y <-> ( x ,~ `' A y /\ x ,~ `' B y ) ) )
2 1 el2v 
 |-  ( x ,~ `' ( A |X. B ) y <-> ( x ,~ `' A y /\ x ,~ `' B y ) )
3 2 opabbii 
 |-  { <. x , y >. | x ,~ `' ( A |X. B ) y } = { <. x , y >. | ( x ,~ `' A y /\ x ,~ `' B y ) }
4 inopab 
 |-  ( { <. x , y >. | x ,~ `' A y } i^i { <. x , y >. | x ,~ `' B y } ) = { <. x , y >. | ( x ,~ `' A y /\ x ,~ `' B y ) }
5 3 4 eqtr4i 
 |-  { <. x , y >. | x ,~ `' ( A |X. B ) y } = ( { <. x , y >. | x ,~ `' A y } i^i { <. x , y >. | x ,~ `' B y } )
6 relcoss 
 |-  Rel ,~ `' ( A |X. B )
7 dfrel4v 
 |-  ( Rel ,~ `' ( A |X. B ) <-> ,~ `' ( A |X. B ) = { <. x , y >. | x ,~ `' ( A |X. B ) y } )
8 6 7 mpbi 
 |-  ,~ `' ( A |X. B ) = { <. x , y >. | x ,~ `' ( A |X. B ) y }
9 relcoss 
 |-  Rel ,~ `' A
10 dfrel4v 
 |-  ( Rel ,~ `' A <-> ,~ `' A = { <. x , y >. | x ,~ `' A y } )
11 9 10 mpbi 
 |-  ,~ `' A = { <. x , y >. | x ,~ `' A y }
12 relcoss 
 |-  Rel ,~ `' B
13 dfrel4v 
 |-  ( Rel ,~ `' B <-> ,~ `' B = { <. x , y >. | x ,~ `' B y } )
14 12 13 mpbi 
 |-  ,~ `' B = { <. x , y >. | x ,~ `' B y }
15 11 14 ineq12i 
 |-  ( ,~ `' A i^i ,~ `' B ) = ( { <. x , y >. | x ,~ `' A y } i^i { <. x , y >. | x ,~ `' B y } )
16 5 8 15 3eqtr4i 
 |-  ,~ `' ( A |X. B ) = ( ,~ `' A i^i ,~ `' B )