Metamath Proof Explorer

Theorem bren

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998) (Proof shortened by BTernaryTau, 23-Sep-2024)

Ref Expression
Assertion bren 
|- ( A ~~ B <-> E. f f : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 encv 
 |-  ( A ~~ B -> ( A e. _V /\ B e. _V ) )
2 f1ofn 
 |-  ( f : A -1-1-onto-> B -> f Fn A )
3 fndm 
 |-  ( f Fn A -> dom f = A )
4 vex 
 |-  f e. _V
5 4 dmex 
 |-  dom f e. _V
6 3 5 eqeltrrdi 
 |-  ( f Fn A -> A e. _V )
7 2 6 syl 
 |-  ( f : A -1-1-onto-> B -> A e. _V )
8 f1ofo 
 |-  ( f : A -1-1-onto-> B -> f : A -onto-> B )
9 forn 
 |-  ( f : A -onto-> B -> ran f = B )
10 8 9 syl 
 |-  ( f : A -1-1-onto-> B -> ran f = B )
11 4 rnex 
 |-  ran f e. _V
12 10 11 eqeltrrdi 
 |-  ( f : A -1-1-onto-> B -> B e. _V )
13 7 12 jca 
 |-  ( f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
14 13 exlimiv 
 |-  ( E. f f : A -1-1-onto-> B -> ( A e. _V /\ B e. _V ) )
15 breng 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
16 1 14 15 pm5.21nii 
 |-  ( A ~~ B <-> E. f f : A -1-1-onto-> B )