Metamath Proof Explorer

Theorem numth

Description: Numeration theorem: every set can be put into one-to-one correspondence with some ordinal (using AC). Theorem 10.3 of TakeutiZaring p. 84. (Contributed by NM, 10-Feb-1997) (Proof shortened by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypothesis numth.1 ⊢ A ∈ V
Assertion numth ⊢ ∃ x ∈ On ∃ f f : x ⟶ 1-1 onto A

Proof

Step Hyp Ref Expression
1 numth.1 ⊢ A ∈ V
2 1 numth2 ⊢ ∃ x ∈ On x ≈ A
3 bren ⊢ x ≈ A ↔ ∃ f f : x ⟶ 1-1 onto A
4 3 rexbii ⊢ ∃ x ∈ On x ≈ A ↔ ∃ x ∈ On ∃ f f : x ⟶ 1-1 onto A
5 2 4 mpbi ⊢ ∃ x ∈ On ∃ f f : x ⟶ 1-1 onto A