Theorem relcnveq2

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019)

	Ref	Expression
Assertion	relcnveq2	⊢ ( Rel 𝑅 → ( ◡ 𝑅 = 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnvsym	⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )
2	1	a1i	⊢ ( Rel 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) )
3		dfrel2	⊢ ( Rel 𝑅 ↔ ◡ ◡ 𝑅 = 𝑅 )
4	3	biimpi	⊢ ( Rel 𝑅 → ◡ ◡ 𝑅 = 𝑅 )
5	4	sseq1d	⊢ ( Rel 𝑅 → ( ◡ ◡ 𝑅 ⊆ ◡ 𝑅 ↔ 𝑅 ⊆ ◡ 𝑅 ) )
6		cnvsym	⊢ ( ◡ ◡ 𝑅 ⊆ ◡ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ◡ 𝑅 𝑦 → 𝑦 ◡ 𝑅 𝑥 ) )
7	5 6	bitr3di	⊢ ( Rel 𝑅 → ( 𝑅 ⊆ ◡ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ◡ 𝑅 𝑦 → 𝑦 ◡ 𝑅 𝑥 ) ) )
8		relbrcnvg	⊢ ( Rel 𝑅 → ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) )
9		relbrcnvg	⊢ ( Rel 𝑅 → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
10	8 9	imbi12d	⊢ ( Rel 𝑅 → ( ( 𝑥 ◡ 𝑅 𝑦 → 𝑦 ◡ 𝑅 𝑥 ) ↔ ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) )
11	10	2albidv	⊢ ( Rel 𝑅 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ◡ 𝑅 𝑦 → 𝑦 ◡ 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) )
12	7 11	bitrd	⊢ ( Rel 𝑅 → ( 𝑅 ⊆ ◡ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) )
13	2 12	anbi12d	⊢ ( Rel 𝑅 → ( ( ◡ 𝑅 ⊆ 𝑅 ∧ 𝑅 ⊆ ◡ 𝑅 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) ) )
14		eqss	⊢ ( ◡ 𝑅 = 𝑅 ↔ ( ◡ 𝑅 ⊆ 𝑅 ∧ 𝑅 ⊆ ◡ 𝑅 ) )
15		2albiim	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 𝑅 𝑥 → 𝑥 𝑅 𝑦 ) ) )
16	13 14 15	3bitr4g	⊢ ( Rel 𝑅 → ( ◡ 𝑅 = 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) ) )