Metamath Proof Explorer

Theorem isnum2

Description: A way to express well-orderability without bound or distinct variables. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by Mario Carneiro, 27-Apr-2015)

		Ref	Expression
	Assertion	isnum2	$⊢ A \in dom card \leftrightarrow \exists x \in On x \approx A$

Proof

Step	Hyp	Ref	Expression
1		cardf2	$⊢ card : \{y \| \exists x \in On x \approx y\} ⟶ On$
2	1	fdmi	$⊢ dom card = \{y \| \exists x \in On x \approx y\}$
3	2	eleq2i	$⊢ A \in dom card \leftrightarrow A \in \{y \| \exists x \in On x \approx y\}$
4		relen	$⊢ Rel \approx$
5	4	brrelex2i	$⊢ x \approx A \to A \in V$
6	5	rexlimivw	$⊢ \exists x \in On x \approx A \to A \in V$
7		breq2	$⊢ y = A \to (x \approx y \leftrightarrow x \approx A)$
8	7	rexbidv	$⊢ y = A \to (\exists x \in On x \approx y \leftrightarrow \exists x \in On x \approx A)$
9	6 8	elab3	$⊢ A \in \{y \| \exists x \in On x \approx y\} \leftrightarrow \exists x \in On x \approx A$
10	3 9	bitri	$⊢ A \in dom card \leftrightarrow \exists x \in On x \approx A$