This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → B C ≀ R ⋉ S ↾ A D E ↔ ∃ u ∈ A u S C ∧ u R B ∧ u S E ∧ u R D

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 ⊢ B C ≀ R ⋉ S ↾ A D E ↔ B C ≀ R ⋉ S ↾ A D E
4 opex ⊢ B C ∈ V
5 opex ⊢ D E ∈ V
6 br1cossres ⊢ B C ∈ V ∧ D E ∈ V → B C ≀ R ⋉ S ↾ A D E ↔ ∃ u ∈ A u R ⋉ S B C ∧ u R ⋉ S D E
7 4 5 6 mp2an ⊢ B C ≀ R ⋉ S ↾ A D E ↔ ∃ u ∈ A u R ⋉ S B C ∧ u R ⋉ S D E
8 brxrn ⊢ u ∈ V ∧ B ∈ V ∧ C ∈ W → u R ⋉ S B C ↔ u R B ∧ u S C
9 8 el3v1 ⊢ B ∈ V ∧ C ∈ W → u R ⋉ S B C ↔ u R B ∧ u S C
10 brxrn ⊢ u ∈ V ∧ D ∈ X ∧ E ∈ Y → u R ⋉ S D E ↔ u R D ∧ u S E
11 10 el3v1 ⊢ D ∈ X ∧ E ∈ Y → u R ⋉ S D E ↔ u R D ∧ u S E
12 9 11 bi2anan9 ⊢ B ∈ V ∧ C ∈ W ∧ D ∈ X ∧ E ∈ Y → u R ⋉ S B C ∧ u R ⋉ S D E ↔ u R B ∧ u S C ∧ u R D ∧ u S E
13 an2anr ⊢ u R B ∧ u S C ∧ u R D ∧ u S E ↔ u S C ∧ u R B ∧ u S E ∧ u R D
14 12 13 bitrdi ⊢ B ∈ V ∧ C ∈ W ∧ D ∈ X ∧ E ∈ Y → u R ⋉ S B C ∧ u R ⋉ S D E ↔ u S C ∧ u R B ∧ u S E ∧ u R D
15 14 rexbidv ⊢ B ∈ V ∧ C ∈ W ∧ D ∈ X ∧ E ∈ Y → ∃ u ∈ A u R ⋉ S B C ∧ u R ⋉ S D E ↔ ∃ u ∈ A u S C ∧ u R B ∧ u S E ∧ u R D
16 7 15 bitrid ⊢ B ∈ V ∧ C ∈ W ∧ D ∈ X ∧ E ∈ Y → B C ≀ R ⋉ S ↾ A D E ↔ ∃ u ∈ A u S C ∧ u R B ∧ u S E ∧ u R D
17 3 16 bitr3id ⊢ B ∈ V ∧ C ∈ W ∧ D ∈ X ∧ E ∈ Y → B C ≀ R ⋉ S ↾ A D E ↔ ∃ u ∈ A u S C ∧ u R B ∧ u S E ∧ u R D