Metamath Proof Explorer


Theorem br1cossxrncnvepres

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

Ref Expression
Assertion br1cossxrncnvepres B V C W D X E Y B C R E -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 E -1 A D E u A u E -1 C u R B u E -1 E u R D
2 brcnvep u V u E -1 C C u
3 2 elv u E -1 C C u
4 3 anbi1i u E -1 C u R B C u u R B
5 brcnvep u V u E -1 E E u
6 5 elv u E -1 E E u
7 6 anbi1i u E -1 E u R D E u u R D
8 4 7 anbi12i u E -1 C u R B u E -1 E u R D C u u R B E u u R D
9 8 rexbii u A u E -1 C u R B u E -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 E -1 A D E u A C u u R B E u u R D