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 ( 𝑅 ∈ Rels → ( 𝑅 = 𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 cnvsym ( 𝑅𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )
2 1 a1i ( 𝑅 ∈ Rels → ( 𝑅𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )
3 elrelsrelim ( 𝑅 ∈ Rels → Rel 𝑅 )
4 dfrel2 ( Rel 𝑅 𝑅 = 𝑅 )
5 3 4 sylib ( 𝑅 ∈ Rels → 𝑅 = 𝑅 )
6 5 sseq1d ( 𝑅 ∈ Rels → ( 𝑅 𝑅𝑅 𝑅 ) )
7 cnvsym ( 𝑅 𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )
8 6 7 bitr3di ( 𝑅 ∈ Rels → ( 𝑅 𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )
9 relbrcnvg ( Rel 𝑅 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )
10 3 9 syl ( 𝑅 ∈ Rels → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )
11 relbrcnvg ( Rel 𝑅 → ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑦 ) )
12 3 11 syl ( 𝑅 ∈ Rels → ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑦 ) )
13 10 12 imbi12d ( 𝑅 ∈ Rels → ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑦 ) ) )
14 13 2albidv ( 𝑅 ∈ Rels → ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥𝑦 ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑦 ) ) )
15 8 14 bitrd ( 𝑅 ∈ Rels → ( 𝑅 𝑅 ↔ ∀ 𝑥𝑦 ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑦 ) ) )
16 2 15 anbi12d ( 𝑅 ∈ Rels → ( ( 𝑅𝑅𝑅 𝑅 ) ↔ ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥𝑦 ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑦 ) ) ) )
17 eqss ( 𝑅 = 𝑅 ↔ ( 𝑅𝑅𝑅 𝑅 ) )
18 2albiim ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥𝑦 ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑦 ) ) )
19 16 17 18 3bitr4g ( 𝑅 ∈ Rels → ( 𝑅 = 𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )