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 f f : A 1-1 onto B

Proof

Step Hyp Ref Expression
1 encv A B A V B V
2 f1ofn f : A 1-1 onto B f Fn A
3 fndm f Fn A dom f = A
4 vex f V
5 4 dmex dom f V
6 3 5 eqeltrrdi f Fn A A V
7 2 6 syl f : A 1-1 onto B A 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 V
12 10 11 eqeltrrdi f : A 1-1 onto B B V
13 7 12 jca f : A 1-1 onto B A V B V
14 13 exlimiv f f : A 1-1 onto B A V B V
15 f1oeq2 x = A f : x 1-1 onto y f : A 1-1 onto y
16 15 exbidv x = A f f : x 1-1 onto y 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 f f : A 1-1 onto y f f : A 1-1 onto B
19 df-en = x y | f f : x 1-1 onto y
20 16 18 19 brabg A V B V A B f f : A 1-1 onto B
21 1 14 20 pm5.21nii A B f f : A 1-1 onto B