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	bitrid	⊢ ( Rel 𝑅 → ( 𝑅 = ◡ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )