Theorem symrelcoss2

Description: The class of cosets by R is symmetric, see dfsymrel2 . (Contributed by Peter Mazsa, 27-Dec-2018)

	Ref	Expression
Assertion	symrelcoss2	⊢ ( ◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		symrelcoss3	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) ∧ Rel ≀ 𝑅 )
2		cnvsym	⊢ ( ◡ ≀ 𝑅 ⊆ ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) )
3	2	anbi1i	⊢ ( ( ◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) ∧ Rel ≀ 𝑅 ) )
4	1 3	mpbir	⊢ ( ◡ ≀ 𝑅 ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅 )