This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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