Metamath Proof Explorer

Theorem bren

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998)

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 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