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→BC≀R⋉S-1↾ADE↔∃u∈AC⊆u∧uRB∧E⊆u∧uRD

Proof

Step Hyp Ref Expression
1 br1cossxrnres ⊢B∈V∧C∈W∧D∈X∧E∈Y→BC≀R⋉S-1↾ADE↔∃u∈AuS-1C∧uRB∧uS-1E∧uRD
2 brcnvssr ⊢u∈V→uS-1C↔C⊆u
3 2 elv ⊢uS-1C↔C⊆u
4 3 anbi1i ⊢uS-1C∧uRB↔C⊆u∧uRB
5 brcnvssr ⊢u∈V→uS-1E↔E⊆u
6 5 elv ⊢uS-1E↔E⊆u
7 6 anbi1i ⊢uS-1E∧uRD↔E⊆u∧uRD
8 4 7 anbi12i ⊢uS-1C∧uRB∧uS-1E∧uRD↔C⊆u∧uRB∧E⊆u∧uRD
9 8 rexbii ⊢∃u∈AuS-1C∧uRB∧uS-1E∧uRD↔∃u∈AC⊆u∧uRB∧E⊆u∧uRD
10 1 9 bitrdi ⊢B∈V∧C∈W∧D∈X∧E∈Y→BC≀R⋉S-1↾ADE↔∃u∈AC⊆u∧uRB∧E⊆u∧uRD