# 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 \mathrm{dom}\mathrm{card}↔\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{x}\approx {A}$

### Proof

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