Theorem dfcoss3

Description: Alternate definition of the class of cosets by R (see the comment of df-coss ). (Contributed by Peter Mazsa, 27-Dec-2018)

	Ref	Expression
Assertion	dfcoss3	⊢ ≀ 𝑅 = ( 𝑅 ∘ ◡ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		brcnvg	⊢ ( ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) → ( 𝑥 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝑥 ) )
2	1	el2v	⊢ ( 𝑥 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝑥 )
3	2	anbi1i	⊢ ( ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑢 𝑅 𝑦 ) ↔ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) )
4	3	exbii	⊢ ( ∃ 𝑢 ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑢 𝑅 𝑦 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) )
5	4	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑢 𝑅 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }
6		df-co	⊢ ( 𝑅 ∘ ◡ 𝑅 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑢 𝑅 𝑦 ) }
7		df-coss	⊢ ≀ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }
8	5 6 7	3eqtr4ri	⊢ ≀ 𝑅 = ( 𝑅 ∘ ◡ 𝑅 )