Metamath Proof Explorer

Theorem coss1cnvres

Description: Class of cosets by the converse of a restriction. (Contributed by Peter Mazsa, 8-Jun-2020)

Ref Expression
Assertion coss1cnvres ⊢ ≀ R ↾ A -1 = u v | u ∈ A ∧ v ∈ A ∧ ∃ x u R x ∧ v R x

Proof

Step Hyp Ref Expression
1 df-coss ⊢ ≀ R ↾ A -1 = u v | ∃ x x R ↾ A -1 u ∧ x R ↾ A -1 v
2 br1cnvres ⊢ x ∈ V → x R ↾ A -1 u ↔ u ∈ A ∧ u R x
3 2 elv ⊢ x R ↾ A -1 u ↔ u ∈ A ∧ u R x
4 br1cnvres ⊢ x ∈ V → x R ↾ A -1 v ↔ v ∈ A ∧ v R x
5 4 elv ⊢ x R ↾ A -1 v ↔ v ∈ A ∧ v R x
6 3 5 anbi12i ⊢ x R ↾ A -1 u ∧ x R ↾ A -1 v ↔ u ∈ A ∧ u R x ∧ v ∈ A ∧ v R x
7 an4 ⊢ u ∈ A ∧ v ∈ A ∧ u R x ∧ v R x ↔ u ∈ A ∧ u R x ∧ v ∈ A ∧ v R x
8 6 7 bitr4i ⊢ x R ↾ A -1 u ∧ x R ↾ A -1 v ↔ u ∈ A ∧ v ∈ A ∧ u R x ∧ v R x
9 8 exbii ⊢ ∃ x x R ↾ A -1 u ∧ x R ↾ A -1 v ↔ ∃ x u ∈ A ∧ v ∈ A ∧ u R x ∧ v R x
10 19.42v ⊢ ∃ x u ∈ A ∧ v ∈ A ∧ u R x ∧ v R x ↔ u ∈ A ∧ v ∈ A ∧ ∃ x u R x ∧ v R x
11 9 10 bitri ⊢ ∃ x x R ↾ A -1 u ∧ x R ↾ A -1 v ↔ u ∈ A ∧ v ∈ A ∧ ∃ x u R x ∧ v R x
12 11 opabbii ⊢ u v | ∃ x x R ↾ A -1 u ∧ x R ↾ A -1 v = u v | u ∈ A ∧ v ∈ A ∧ ∃ x u R x ∧ v R x
13 1 12 eqtri ⊢ ≀ R ↾ A -1 = u v | u ∈ A ∧ v ∈ A ∧ ∃ x u R x ∧ v R x