Metamath Proof Explorer

Theorem elrelscnveq2

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021)

Ref Expression
Assertion elrelscnveq2 ⊢ R ∈ Rels → R -1 = R ↔ ∀ x ∀ y x R y ↔ y R x

Proof

Step Hyp Ref Expression
1 cnvsym ⊢ R -1 ⊆ R ↔ ∀ x ∀ y x R y → y R x
2 1 a1i ⊢ R ∈ Rels → R -1 ⊆ R ↔ ∀ x ∀ y x R y → y R x
3 elrelsrelim ⊢ R ∈ Rels → Rel ⁡ R
4 dfrel2 ⊢ Rel ⁡ R ↔ R -1 -1 = R
5 3 4 sylib ⊢ R ∈ Rels → R -1 -1 = R
6 5 sseq1d ⊢ R ∈ Rels → R -1 -1 ⊆ R -1 ↔ R ⊆ R -1
7 cnvsym ⊢ R -1 -1 ⊆ R -1 ↔ ∀ x ∀ y x R -1 y → y R -1 x
8 6 7 bitr3di ⊢ R ∈ Rels → R ⊆ R -1 ↔ ∀ x ∀ y x R -1 y → y R -1 x
9 relbrcnvg ⊢ Rel ⁡ R → x R -1 y ↔ y R x
10 3 9 syl ⊢ R ∈ Rels → x R -1 y ↔ y R x
11 relbrcnvg ⊢ Rel ⁡ R → y R -1 x ↔ x R y
12 3 11 syl ⊢ R ∈ Rels → y R -1 x ↔ x R y
13 10 12 imbi12d ⊢ R ∈ Rels → x R -1 y → y R -1 x ↔ y R x → x R y
14 13 2albidv ⊢ R ∈ Rels → ∀ x ∀ y x R -1 y → y R -1 x ↔ ∀ x ∀ y y R x → x R y
15 8 14 bitrd ⊢ R ∈ Rels → R ⊆ R -1 ↔ ∀ x ∀ y y R x → x R y
16 2 15 anbi12d ⊢ R ∈ Rels → R -1 ⊆ R ∧ R ⊆ R -1 ↔ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y y R x → x R y
17 eqss ⊢ R -1 = R ↔ R -1 ⊆ R ∧ R ⊆ R -1
18 2albiim ⊢ ∀ x ∀ y x R y ↔ y R x ↔ ∀ x ∀ y x R y → y R x ∧ ∀ x ∀ y y R x → x R y
19 16 17 18 3bitr4g ⊢ R ∈ Rels → R -1 = R ↔ ∀ x ∀ y x R y ↔ y R x