Theorem kardex

Description: The collection of all sets equinumerous to a set A and having the least possible rank is a set. This is the part of the justification of the definition of kard of Enderton p. 222. (Contributed by NM, 14-Dec-2003)

	Ref	Expression
Assertion	kardex	$$⊢\left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$$⊢\left\{x\in \left\{z|z\approx A\right\}|\forall y\in \left\{z|z\approx A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\left\{x|\left(x\in \left\{z|z\approx A\right\}\wedge \forall y\in \left\{z|z\approx A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3		breq1	$$⊢z=x\to \left(z\approx A\leftrightarrow x\approx A\right)$$
4	2 3	elab	$$⊢x\in \left\{z|z\approx A\right\}\leftrightarrow x\approx A$$
5		breq1	$$⊢z=y\to \left(z\approx A\leftrightarrow y\approx A\right)$$
6	5	ralab	$$⊢\forall y\in \left\{z|z\approx A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\leftrightarrow \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
7	4 6	anbi12i	$$⊢\left(x\in \left\{z|z\approx A\right\}\wedge \forall y\in \left\{z|z\approx A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
8	7	abbii	$$⊢\left\{x|\left(x\in \left\{z|z\approx A\right\}\wedge \forall y\in \left\{z|z\approx A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right\}=\left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
9	1 8	eqtri	$$⊢\left\{x\in \left\{z|z\approx A\right\}|\forall y\in \left\{z|z\approx A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}$$
10		scottex	$$⊢\left\{x\in \left\{z|z\approx A\right\}|\forall y\in \left\{z|z\approx A\right\}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}\in \mathrm{V}$$
11	9 10	eqeltrri	$$⊢\left\{x|\left(x\approx A\wedge \forall y\left(y\approx A\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right\}\in \mathrm{V}$$