Theorem cnvsym

Description: Two ways of saying a relation is symmetric. Similar to definition of symmetry in Schechter p. 51. (Contributed by NM, 28-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	cnvsym	⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		alcom	⊢ ( ∀ 𝑦 ∀ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
2		relcnv	⊢ Rel ◡ 𝑅
3		ssrel	⊢ ( Rel ◡ 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑦 ∀ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) ) )
4	2 3	ax-mp	⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑦 ∀ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
5		vex	⊢ 𝑦 ∈ V
6		vex	⊢ 𝑥 ∈ V
7	5 6	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
8		df-br	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 )
9	7 8	bitr3i	⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 )
10		df-br	⊢ ( 𝑦 𝑅 𝑥 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 )
11	9 10	imbi12i	⊢ ( ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
12	11	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 → ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) )
13	1 4 12	3bitr4i	⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )