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

Metamath Proof Explorer

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