Metamath Proof Explorer

Theorem sbthcl

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

Ref Expression
Assertion sbthcl 
|- ~~ = ( ~<_ i^i `' ~<_ )

Proof

Step Hyp Ref Expression
1 relen 
 |-  Rel ~~
2 inss1 
 |-  ( ~<_ i^i `' ~<_ ) C_ ~<_
3 reldom 
 |-  Rel ~<_
4 relss 
 |-  ( ( ~<_ i^i `' ~<_ ) C_ ~<_ -> ( Rel ~<_ -> Rel ( ~<_ i^i `' ~<_ ) ) )
5 2 3 4 mp2 
 |-  Rel ( ~<_ i^i `' ~<_ )
6 brin 
 |-  ( x ( ~<_ i^i `' ~<_ ) y <-> ( x ~<_ y /\ x `' ~<_ y ) )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 brcnv 
 |-  ( x `' ~<_ y <-> y ~<_ x )
10 9 anbi2i 
 |-  ( ( x ~<_ y /\ x `' ~<_ y ) <-> ( x ~<_ y /\ y ~<_ x ) )
11 sbthb 
 |-  ( ( x ~<_ y /\ y ~<_ x ) <-> x ~~ y )
12 6 10 11 3bitrri 
 |-  ( x ~~ y <-> x ( ~<_ i^i `' ~<_ ) y )
13 1 5 12 eqbrriv 
 |-  ~~ = ( ~<_ i^i `' ~<_ )