Theorem cosselrels

Description: Cosets of sets are elements of the relations class. Implies |- ( R e. Rels -> ,R e. Rels ) . (Contributed by Peter Mazsa, 25-Aug-2021)

	Ref	Expression
Assertion	cosselrels	$$⊢A\in V\to \wr A\in \mathrm{Rels}$$

Proof

Step	Hyp	Ref	Expression
1		cossex	$$⊢A\in V\to \wr A\in \mathrm{V}$$
2		relcoss	$$⊢\mathrm{Rel}\wr A$$
3		elrelsrel	$$⊢\wr A\in \mathrm{V}\to \left(\wr A\in \mathrm{Rels}\leftrightarrow \mathrm{Rel}\wr A\right)$$
4	2 3	mpbiri	$$⊢\wr A\in \mathrm{V}\to \wr A\in \mathrm{Rels}$$
5	1 4	syl	$$⊢A\in V\to \wr A\in \mathrm{Rels}$$