Theorem cnvcosseq

Description: The converse of cosets by R are cosets by R . (Contributed by Peter Mazsa, 3-May-2019)

	Ref	Expression
Assertion	cnvcosseq	⊢ ◡ ≀ 𝑅 = ≀ 𝑅

Proof

Step	Hyp	Ref	Expression
1		brcosscnvcoss	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ≀ 𝑅 𝑦 ↔ 𝑦 ≀ 𝑅 𝑥 ) )
2	1	el2v	⊢ ( 𝑥 ≀ 𝑅 𝑦 ↔ 𝑦 ≀ 𝑅 𝑥 )
3	2	biimpi	⊢ ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 )
4	3	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 )
5		cnvsym	⊢ ( ◡ ≀ 𝑅 ⊆ ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) )
6	4 5	mpbir	⊢ ◡ ≀ 𝑅 ⊆ ≀ 𝑅
7		relcoss	⊢ Rel ≀ 𝑅
8		relcnveq	⊢ ( Rel ≀ 𝑅 → ( ◡ ≀ 𝑅 ⊆ ≀ 𝑅 ↔ ◡ ≀ 𝑅 = ≀ 𝑅 ) )
9	7 8	ax-mp	⊢ ( ◡ ≀ 𝑅 ⊆ ≀ 𝑅 ↔ ◡ ≀ 𝑅 = ≀ 𝑅 )
10	6 9	mpbi	⊢ ◡ ≀ 𝑅 = ≀ 𝑅