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 On A ≺ x$

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

Metamath Proof Explorer