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

Metamath Proof Explorer

Theorem numth2

Description: Numeration theorem: any set is equinumerous to some ordinal (using AC). Theorem 10.3 of TakeutiZaring p. 84. (Contributed by NM, 20-Oct-2003)

		Ref	Expression
	Hypothesis	numth.1	⊢ 𝐴 ∈ V
	Assertion	numth2	⊢ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		numth.1	⊢ 𝐴 ∈ V
2		numth3	⊢ ( 𝐴 ∈ V → 𝐴 ∈ dom card )
3	1 2	ax-mp	⊢ 𝐴 ∈ dom card
4		isnum2	⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 )
5	3 4	mpbi	⊢ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴