sbthcl

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

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

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

Metamath Proof Explorer