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 → B C ≀ R ⋉ S -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 ⋉ S -1 ↾ A D E ↔ ∃ u ∈ A u S -1 C ∧ u R B ∧ u S -1 E ∧ u R D
2 brcnvssr ⊢ u ∈ V → u S -1 C ↔ C ⊆ u
3 2 elv ⊢ u S -1 C ↔ C ⊆ u
4 3 anbi1i ⊢ u S -1 C ∧ u R B ↔ C ⊆ u ∧ u R B
5 brcnvssr ⊢ u ∈ V → u S -1 E ↔ E ⊆ u
6 5 elv ⊢ u S -1 E ↔ E ⊆ u
7 6 anbi1i ⊢ u S -1 E ∧ u R D ↔ E ⊆ u ∧ u R D
8 4 7 anbi12i ⊢ u S -1 C ∧ u R B ∧ u S -1 E ∧ u R D ↔ C ⊆ u ∧ u R B ∧ E ⊆ u ∧ u R D
9 8 rexbii ⊢ ∃ u ∈ A u S -1 C ∧ u R B ∧ u S -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 ⋉ S -1 ↾ A D E ↔ ∃ u ∈ A C ⊆ u ∧ u R B ∧ E ⊆ u ∧ u R D