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

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