Theorem sbthcl

Description: Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998)

	Ref	Expression
Assertion	sbthcl	$$⊢\approx =\preccurlyeq \cap {\preccurlyeq }^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		relen	$$⊢\mathrm{Rel}\approx$$
2		inss1	$$⊢\preccurlyeq \cap {\preccurlyeq }^{-1}\subseteq \preccurlyeq$$
3		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
4		relss	$$⊢\preccurlyeq \cap {\preccurlyeq }^{-1}\subseteq \preccurlyeq \to \left(\mathrm{Rel}\preccurlyeq \to \mathrm{Rel}\left(\preccurlyeq \cap {\preccurlyeq }^{-1}\right)\right)$$
5	2 3 4	mp2	$$⊢\mathrm{Rel}\left(\preccurlyeq \cap {\preccurlyeq }^{-1}\right)$$
6		brin	$$⊢x\left(\preccurlyeq \cap {\preccurlyeq }^{-1}\right)y\leftrightarrow \left(x\preccurlyeq y\wedge x{\preccurlyeq }^{-1}y\right)$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	brcnv	$$⊢x{\preccurlyeq }^{-1}y\leftrightarrow y\preccurlyeq x$$
10	9	anbi2i	$$⊢\left(x\preccurlyeq y\wedge x{\preccurlyeq }^{-1}y\right)\leftrightarrow \left(x\preccurlyeq y\wedge y\preccurlyeq x\right)$$
11		sbthb	$$⊢\left(x\preccurlyeq y\wedge y\preccurlyeq x\right)\leftrightarrow x\approx y$$
12	6 10 11	3bitrri	$$⊢x\approx y\leftrightarrow x\left(\preccurlyeq \cap {\preccurlyeq }^{-1}\right)y$$
13	1 5 12	eqbrriv	$$⊢\approx =\preccurlyeq \cap {\preccurlyeq }^{-1}$$