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 ABff:A1-1 ontoB

Proof

Step Hyp Ref Expression
1 encv ABAVBV
2 f1ofn f:A1-1 ontoBfFnA
3 fndm fFnAdomf=A
4 vex fV
5 4 dmex domfV
6 3 5 eqeltrrdi fFnAAV
7 2 6 syl f:A1-1 ontoBAV
8 f1ofo f:A1-1 ontoBf:AontoB
9 forn f:AontoBranf=B
10 8 9 syl f:A1-1 ontoBranf=B
11 4 rnex ranfV
12 10 11 eqeltrrdi f:A1-1 ontoBBV
13 7 12 jca f:A1-1 ontoBAVBV
14 13 exlimiv ff:A1-1 ontoBAVBV
15 breng AVBVABff:A1-1 ontoB
16 1 14 15 pm5.21nii ABff:A1-1 ontoB