Metamath Proof Explorer


Theorem br1cossxrncnvssrres

Description: <. B , C >. and <. D , E >. are cosets by range Cartesian product with restricted converse subsets class: a binary relation. (Contributed by Peter Mazsa, 9-Jun-2021)

Ref Expression
Assertion br1cossxrncnvssrres B V C W D X E Y B C R S -1 A D E u A C u u R B E u u R D

Proof

Step Hyp Ref Expression
1 br1cossxrnres B V C W D X E Y B C R S -1 A D E u A u S -1 C u R B u S -1 E u R D
2 brcnvssr u V u S -1 C C u
3 2 elv u S -1 C C u
4 3 anbi1i u S -1 C u R B C u u R B
5 brcnvssr u V u S -1 E E u
6 5 elv u S -1 E E u
7 6 anbi1i u S -1 E u R D E u u R D
8 4 7 anbi12i u S -1 C u R B u S -1 E u R D C u u R B E u u R D
9 8 rexbii u A u S -1 C u R B u S -1 E u R D u A C u u R B E u u R D
10 1 9 bitrdi B V C W D X E Y B C R S -1 A D E u A C u u R B E u u R D