Theorem numthcor

Description: Any set is strictly dominated by some ordinal. (Contributed by NM, 22-Oct-2003)

	Ref	Expression
Assertion	numthcor	$$⊢A\in V\to \exists x\in \mathrm{On}A\prec x$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢y=A\to \left(y\prec x\leftrightarrow A\prec x\right)$$
2	1	rexbidv	$$⊢y=A\to \left(\exists x\in \mathrm{On}y\prec x\leftrightarrow \exists x\in \mathrm{On}A\prec x\right)$$
3		vpwex	$$⊢𝒫y\in \mathrm{V}$$
4	3	numth2	$$⊢\exists x\in \mathrm{On}x\approx 𝒫y$$
5		vex	$$⊢y\in \mathrm{V}$$
6	5	canth2	$$⊢y\prec 𝒫y$$
7		ensym	$$⊢x\approx 𝒫y\to 𝒫y\approx x$$
8		sdomentr	$$⊢\left(y\prec 𝒫y\wedge 𝒫y\approx x\right)\to y\prec x$$
9	6 7 8	sylancr	$$⊢x\approx 𝒫y\to y\prec x$$
10	9	reximi	$$⊢\exists x\in \mathrm{On}x\approx 𝒫y\to \exists x\in \mathrm{On}y\prec x$$
11	4 10	ax-mp	$$⊢\exists x\in \mathrm{On}y\prec x$$
12	2 11	vtoclg	$$⊢A\in V\to \exists x\in \mathrm{On}A\prec x$$