Theorem sbthcl

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

	Ref	Expression
Assertion	sbthcl	⊢ ≈ = ( ≼ ∩ ◡ ≼ )

Proof

Step	Hyp	Ref	Expression
1		relen	⊢ Rel ≈
2		inss1	⊢ ( ≼ ∩ ◡ ≼ ) ⊆ ≼
3		reldom	⊢ Rel ≼
4		relss	⊢ ( ( ≼ ∩ ◡ ≼ ) ⊆ ≼ → ( Rel ≼ → Rel ( ≼ ∩ ◡ ≼ ) ) )
5	2 3 4	mp2	⊢ Rel ( ≼ ∩ ◡ ≼ )
6		brin	⊢ ( 𝑥 ( ≼ ∩ ◡ ≼ ) 𝑦 ↔ ( 𝑥 ≼ 𝑦 ∧ 𝑥 ◡ ≼ 𝑦 ) )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	brcnv	⊢ ( 𝑥 ◡ ≼ 𝑦 ↔ 𝑦 ≼ 𝑥 )
10	9	anbi2i	⊢ ( ( 𝑥 ≼ 𝑦 ∧ 𝑥 ◡ ≼ 𝑦 ) ↔ ( 𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥 ) )
11		sbthb	⊢ ( ( 𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥 ) ↔ 𝑥 ≈ 𝑦 )
12	6 10 11	3bitrri	⊢ ( 𝑥 ≈ 𝑦 ↔ 𝑥 ( ≼ ∩ ◡ ≼ ) 𝑦 )
13	1 5 12	eqbrriv	⊢ ≈ = ( ≼ ∩ ◡ ≼ )