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 ↔ ∃ 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 breng ⊢ A ∈ V ∧ B ∈ V → A ≈ B ↔ ∃ f f : A ⟶ 1-1 onto B
16 1 14 15 pm5.21nii ⊢ A ≈ B ↔ ∃ f f : A ⟶ 1-1 onto B