Theorem cosscnvelrels

Description: Cosets of converse sets are elements of the relations class. (Contributed by Peter Mazsa, 31-Aug-2021)

	Ref	Expression
Assertion	cosscnvelrels	$$⊢A\in V\to \wr A^{-1}\in \mathrm{Rels}$$

Proof

Step	Hyp	Ref	Expression
1		cnvelrels	$$⊢A\in V\to A^{-1}\in \mathrm{Rels}$$
2		cosselrels	$$⊢A^{-1}\in \mathrm{Rels}\to \wr A^{-1}\in \mathrm{Rels}$$
3	1 2	syl	$$⊢A\in V\to \wr A^{-1}\in \mathrm{Rels}$$