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

Metamath Proof Explorer

Theorem br1cosscnvxrn

Description: A and B are cosets by the converse range Cartesian product: a binary relation. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

Ref Expression
Assertion br1cosscnvxrn ⊢ A ∈ V ∧ B ∈ W → A ≀ R ⋉ S -1 B ↔ A ≀ R -1 B ∧ A ≀ S -1 B

Proof

Step Hyp Ref Expression
1 ecxrn ⊢ A ∈ V → A R ⋉ S = x y | A R x ∧ A S y
2 ecxrn ⊢ B ∈ W → B R ⋉ S = x y | B R x ∧ B S y
3 1 2 ineqan12d ⊢ A ∈ V ∧ B ∈ W → A R ⋉ S ∩ B R ⋉ S = x y | A R x ∧ A S y ∩ x y | B R x ∧ B S y
4 inopab ⊢ x y | A R x ∧ A S y ∩ x y | B R x ∧ B S y = x y | A R x ∧ A S y ∧ B R x ∧ B S y
5 3 4 eqtrdi ⊢ A ∈ V ∧ B ∈ W → A R ⋉ S ∩ B R ⋉ S = x y | A R x ∧ A S y ∧ B R x ∧ B S y
6 an4 ⊢ A R x ∧ A S y ∧ B R x ∧ B S y ↔ A R x ∧ B R x ∧ A S y ∧ B S y
7 6 opabbii ⊢ x y | A R x ∧ A S y ∧ B R x ∧ B S y = x y | A R x ∧ B R x ∧ A S y ∧ B S y
8 5 7 eqtrdi ⊢ A ∈ V ∧ B ∈ W → A R ⋉ S ∩ B R ⋉ S = x y | A R x ∧ B R x ∧ A S y ∧ B S y
9 8 neeq1d ⊢ A ∈ V ∧ B ∈ W → A R ⋉ S ∩ B R ⋉ S ≠ ∅ ↔ x y | A R x ∧ B R x ∧ A S y ∧ B S y ≠ ∅
10 opabn0 ⊢ x y | A R x ∧ B R x ∧ A S y ∧ B S y ≠ ∅ ↔ ∃ x ∃ y A R x ∧ B R x ∧ A S y ∧ B S y
11 exdistrv ⊢ ∃ x ∃ y A R x ∧ B R x ∧ A S y ∧ B S y ↔ ∃ x A R x ∧ B R x ∧ ∃ y A S y ∧ B S y
12 10 11 bitri ⊢ x y | A R x ∧ B R x ∧ A S y ∧ B S y ≠ ∅ ↔ ∃ x A R x ∧ B R x ∧ ∃ y A S y ∧ B S y
13 9 12 bitrdi ⊢ A ∈ V ∧ B ∈ W → A R ⋉ S ∩ B R ⋉ S ≠ ∅ ↔ ∃ x A R x ∧ B R x ∧ ∃ y A S y ∧ B S y
14 brcosscnv2 ⊢ A ∈ V ∧ B ∈ W → A ≀ R ⋉ S -1 B ↔ A R ⋉ S ∩ B R ⋉ S ≠ ∅
15 brcosscnv ⊢ A ∈ V ∧ B ∈ W → A ≀ R -1 B ↔ ∃ x A R x ∧ B R x
16 brcosscnv ⊢ A ∈ V ∧ B ∈ W → A ≀ S -1 B ↔ ∃ y A S y ∧ B S y
17 15 16 anbi12d ⊢ A ∈ V ∧ B ∈ W → A ≀ R -1 B ∧ A ≀ S -1 B ↔ ∃ x A R x ∧ B R x ∧ ∃ y A S y ∧ B S y
18 13 14 17 3bitr4d ⊢ A ∈ V ∧ B ∈ W → A ≀ R ⋉ S -1 B ↔ A ≀ R -1 B ∧ A ≀ S -1 B