Metamath Proof Explorer

Theorem br1cossxrncnvepres

Description: <. B , C >. and <. D , E >. are cosets by a range Cartesian product with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 12-May-2021)

Ref Expression
Assertion br1cossxrncnvepres ⊢ B ∈ V ∧ C ∈ W ∧ D ∈ X ∧ E ∈ Y → B C ≀ R ⋉ E -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 ⋉ E -1 ↾ A D E ↔ ∃ u ∈ A u E -1 C ∧ u R B ∧ u E -1 E ∧ u R D
2 brcnvep ⊢ u ∈ V → u E -1 C ↔ C ∈ u
3 2 elv ⊢ u E -1 C ↔ C ∈ u
4 3 anbi1i ⊢ u E -1 C ∧ u R B ↔ C ∈ u ∧ u R B
5 brcnvep ⊢ u ∈ V → u E -1 E ↔ E ∈ u
6 5 elv ⊢ u E -1 E ↔ E ∈ u
7 6 anbi1i ⊢ u E -1 E ∧ u R D ↔ E ∈ u ∧ u R D
8 4 7 anbi12i ⊢ u E -1 C ∧ u R B ∧ u E -1 E ∧ u R D ↔ C ∈ u ∧ u R B ∧ E ∈ u ∧ u R D
9 8 rexbii ⊢ ∃ u ∈ A u E -1 C ∧ u R B ∧ u E -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 ⋉ E -1 ↾ A D E ↔ ∃ u ∈ A C ∈ u ∧ u R B ∧ E ∈ u ∧ u R D