This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ 𝐴 ∈ V
	Assertion	numth	⊢ ∃ 𝑥 ∈ On ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝐴

Proof

Step	Hyp	Ref	Expression
1		numth.1	⊢ 𝐴 ∈ V
2	1	numth2	⊢ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴
3		bren	⊢ ( 𝑥 ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝐴 )
4	3	rexbii	⊢ ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 ↔ ∃ 𝑥 ∈ On ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝐴 )
5	2 4	mpbi	⊢ ∃ 𝑥 ∈ On ∃ 𝑓 𝑓 : 𝑥 –1-1-onto→ 𝐴