Theorem cosscnvid

Description: Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021)

	Ref	Expression
Assertion	cosscnvid	$$⊢\wr {\mathrm{I}}^{-1}=\mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		cnvi	$$⊢{\mathrm{I}}^{-1}=\mathrm{I}$$
2	1	cosseqi	$$⊢\wr {\mathrm{I}}^{-1}=\wr \mathrm{I}$$
3		cossid	$$⊢\wr \mathrm{I}=\mathrm{I}$$
4	2 3	eqtri	$$⊢\wr {\mathrm{I}}^{-1}=\mathrm{I}$$