Metamath Proof Explorer


Theorem relcnveq3

Description: Two ways of saying a relation is symmetric. (Contributed by FL, 31-Aug-2009)

Ref Expression
Assertion relcnveq3 ( Rel 𝑅 → ( 𝑅 = 𝑅 ↔ ∀ 𝑥𝑦 ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )

Proof

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