Metamath Proof Explorer

Theorem sbthfi

Description: Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth ). (Contributed by BTernaryTau, 4-Nov-2024)

Ref Expression
Assertion sbthfi 
|- ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) -> A ~~ B )

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex1i 
 |-  ( A ~<_ B -> A e. _V )
3 1 brrelex1i 
 |-  ( B ~<_ A -> B e. _V )
4 breq1 
 |-  ( z = A -> ( z ~<_ w <-> A ~<_ w ) )
5 breq2 
 |-  ( z = A -> ( w ~<_ z <-> w ~<_ A ) )
6 4 5 3anbi23d 
 |-  ( z = A -> ( ( w e. Fin /\ z ~<_ w /\ w ~<_ z ) <-> ( w e. Fin /\ A ~<_ w /\ w ~<_ A ) ) )
7 breq1 
 |-  ( z = A -> ( z ~~ w <-> A ~~ w ) )
8 6 7 imbi12d 
 |-  ( z = A -> ( ( ( w e. Fin /\ z ~<_ w /\ w ~<_ z ) -> z ~~ w ) <-> ( ( w e. Fin /\ A ~<_ w /\ w ~<_ A ) -> A ~~ w ) ) )
9 eleq1 
 |-  ( w = B -> ( w e. Fin <-> B e. Fin ) )
10 breq2 
 |-  ( w = B -> ( A ~<_ w <-> A ~<_ B ) )
11 breq1 
 |-  ( w = B -> ( w ~<_ A <-> B ~<_ A ) )
12 9 10 11 3anbi123d 
 |-  ( w = B -> ( ( w e. Fin /\ A ~<_ w /\ w ~<_ A ) <-> ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) ) )
13 breq2 
 |-  ( w = B -> ( A ~~ w <-> A ~~ B ) )
14 12 13 imbi12d 
 |-  ( w = B -> ( ( ( w e. Fin /\ A ~<_ w /\ w ~<_ A ) -> A ~~ w ) <-> ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) -> A ~~ B ) ) )
15 vex 
 |-  z e. _V
16 sseq1 
 |-  ( y = x -> ( y C_ z <-> x C_ z ) )
17 imaeq2 
 |-  ( y = x -> ( f " y ) = ( f " x ) )
18 17 difeq2d 
 |-  ( y = x -> ( w \ ( f " y ) ) = ( w \ ( f " x ) ) )
19 18 imaeq2d 
 |-  ( y = x -> ( g " ( w \ ( f " y ) ) ) = ( g " ( w \ ( f " x ) ) ) )
20 difeq2 
 |-  ( y = x -> ( z \ y ) = ( z \ x ) )
21 19 20 sseq12d 
 |-  ( y = x -> ( ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) <-> ( g " ( w \ ( f " x ) ) ) C_ ( z \ x ) ) )
22 16 21 anbi12d 
 |-  ( y = x -> ( ( y C_ z /\ ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) ) <-> ( x C_ z /\ ( g " ( w \ ( f " x ) ) ) C_ ( z \ x ) ) ) )
23 22 cbvabv 
 |-  { y | ( y C_ z /\ ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) ) } = { x | ( x C_ z /\ ( g " ( w \ ( f " x ) ) ) C_ ( z \ x ) ) }
24 eqid 
 |-  ( ( f |` U. { y | ( y C_ z /\ ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) ) } ) u. ( `' g |` ( z \ U. { y | ( y C_ z /\ ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) ) } ) ) ) = ( ( f |` U. { y | ( y C_ z /\ ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) ) } ) u. ( `' g |` ( z \ U. { y | ( y C_ z /\ ( g " ( w \ ( f " y ) ) ) C_ ( z \ y ) ) } ) ) )
25 vex 
 |-  w e. _V
26 15 23 24 25 sbthfilem 
 |-  ( ( w e. Fin /\ z ~<_ w /\ w ~<_ z ) -> z ~~ w )
27 8 14 26 vtocl2g 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) -> A ~~ B ) )
28 2 3 27 syl2an 
 |-  ( ( A ~<_ B /\ B ~<_ A ) -> ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) -> A ~~ B ) )
29 28 3adant1 
 |-  ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) -> ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) -> A ~~ B ) )
30 29 pm2.43i 
 |-  ( ( B e. Fin /\ A ~<_ B /\ B ~<_ A ) -> A ~~ B )