Metamath Proof Explorer


Theorem br1cossinres

Description: B and C are cosets by an intersection with a restriction: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion br1cossinres B V C W B R S A C u A u S B u R B u S C u R C

Proof

Step Hyp Ref Expression
1 inres R S A = R S A
2 1 cosseqi R S A = R S A
3 2 breqi B R S A C B R S A C
4 br1cossres B V C W B R S A C u A u R S B u R S C
5 brin u R S B u R B u S B
6 brin u R S C u R C u S C
7 5 6 anbi12i u R S B u R S C u R B u S B u R C u S C
8 an2anr u R B u S B u R C u S C u S B u R B u S C u R C
9 7 8 bitri u R S B u R S C u S B u R B u S C u R C
10 9 rexbii u A u R S B u R S C u A u S B u R B u S C u R C
11 4 10 bitrdi B V C W B R S A C u A u S B u R B u S C u R C
12 3 11 syl5bb B V C W B R S A C u A u S B u R B u S C u R C