Metamath Proof Explorer

Theorem br1cossxrnres

Description: <. B , C >. and <. D , E >. are cosets by an range Cartesian product with a restriction: a binary relation. (Contributed by Peter Mazsa, 8-Jun-2021)

Ref Expression
Assertion br1cossxrnres ⊢B∈V∧C∈W∧D∈X∧E∈Y→BC≀R⋉S↾ADE↔∃u∈AuSC∧uRB∧uSE∧uRD

Proof

Step Hyp Ref Expression
1 xrnres2 ⊢R⋉S↾A=R⋉S↾A
2 1 cosseqi ⊢≀R⋉S↾A=≀R⋉S↾A
3 2 breqi ⊢BC≀R⋉S↾ADE↔BC≀R⋉S↾ADE
4 opex ⊢BC∈V
5 opex ⊢DE∈V
6 br1cossres ⊢BC∈V∧DE∈V→BC≀R⋉S↾ADE↔∃u∈AuR⋉SBC∧uR⋉SDE
7 4 5 6 mp2an ⊢BC≀R⋉S↾ADE↔∃u∈AuR⋉SBC∧uR⋉SDE
8 brxrn ⊢u∈V∧B∈V∧C∈W→uR⋉SBC↔uRB∧uSC
9 8 el3v1 ⊢B∈V∧C∈W→uR⋉SBC↔uRB∧uSC
10 brxrn ⊢u∈V∧D∈X∧E∈Y→uR⋉SDE↔uRD∧uSE
11 10 el3v1 ⊢D∈X∧E∈Y→uR⋉SDE↔uRD∧uSE
12 9 11 bi2anan9 ⊢B∈V∧C∈W∧D∈X∧E∈Y→uR⋉SBC∧uR⋉SDE↔uRB∧uSC∧uRD∧uSE
13 an2anr ⊢uRB∧uSC∧uRD∧uSE↔uSC∧uRB∧uSE∧uRD
14 12 13 bitrdi ⊢B∈V∧C∈W∧D∈X∧E∈Y→uR⋉SBC∧uR⋉SDE↔uSC∧uRB∧uSE∧uRD
15 14 rexbidv ⊢B∈V∧C∈W∧D∈X∧E∈Y→∃u∈AuR⋉SBC∧uR⋉SDE↔∃u∈AuSC∧uRB∧uSE∧uRD
16 7 15 bitrid ⊢B∈V∧C∈W∧D∈X∧E∈Y→BC≀R⋉S↾ADE↔∃u∈AuSC∧uRB∧uSE∧uRD
17 3 16 bitr3id ⊢B∈V∧C∈W∧D∈X∧E∈Y→BC≀R⋉S↾ADE↔∃u∈AuSC∧uRB∧uSE∧uRD