Metamath Proof Explorer


Theorem elrelscnveq3

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

Ref Expression
Assertion elrelscnveq3 ( 𝑅 ∈ Rels → ( 𝑅 = 𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 eqss ( 𝑅 = 𝑅 ↔ ( 𝑅 𝑅 𝑅𝑅 ) )
2 cnvsym ( 𝑅𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )
3 2 biimpi ( 𝑅𝑅 → ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )
4 3 a1d ( 𝑅𝑅 → ( 𝑅 ∈ Rels → ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )
5 4 adantl ( ( 𝑅 𝑅 𝑅𝑅 ) → ( 𝑅 ∈ Rels → ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )
6 5 com12 ( 𝑅 ∈ Rels → ( ( 𝑅 𝑅 𝑅𝑅 ) → ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )
7 elrelsrelim ( 𝑅 ∈ Rels → Rel 𝑅 )
8 dfrel2 ( Rel 𝑅 𝑅 = 𝑅 )
9 7 8 sylib ( 𝑅 ∈ Rels → 𝑅 = 𝑅 )
10 cnvss ( 𝑅𝑅 𝑅 𝑅 )
11 sseq1 ( 𝑅 = 𝑅 → ( 𝑅 𝑅𝑅 𝑅 ) )
12 10 11 syl5ibcom ( 𝑅𝑅 → ( 𝑅 = 𝑅𝑅 𝑅 ) )
13 2 12 sylbir ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → ( 𝑅 = 𝑅𝑅 𝑅 ) )
14 9 13 syl5com ( 𝑅 ∈ Rels → ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑅 𝑅 ) )
15 2 biimpri ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑅𝑅 )
16 14 15 jca2 ( 𝑅 ∈ Rels → ( ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → ( 𝑅 𝑅 𝑅𝑅 ) ) )
17 6 16 impbid ( 𝑅 ∈ Rels → ( ( 𝑅 𝑅 𝑅𝑅 ) ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )
18 1 17 syl5bb ( 𝑅 ∈ Rels → ( 𝑅 = 𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )