Metamath Proof Explorer


Theorem brenOLD

Description: Obsolete version of bren as of 23-Sep-2024. (Contributed by NM, 15-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion brenOLD
|- ( 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 f1oeq2
 |-  ( x = A -> ( f : x -1-1-onto-> y <-> f : A -1-1-onto-> y ) )
16 15 exbidv
 |-  ( x = A -> ( E. f f : x -1-1-onto-> y <-> E. f f : A -1-1-onto-> y ) )
17 f1oeq3
 |-  ( y = B -> ( f : A -1-1-onto-> y <-> f : A -1-1-onto-> B ) )
18 17 exbidv
 |-  ( y = B -> ( E. f f : A -1-1-onto-> y <-> E. f f : A -1-1-onto-> B ) )
19 df-en
 |-  ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
20 16 18 19 brabg
 |-  ( ( A e. _V /\ B e. _V ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
21 1 14 20 pm5.21nii
 |-  ( A ~~ B <-> E. f f : A -1-1-onto-> B )