Theorem cardmin

Description: The smallest ordinal that strictly dominates a set is a cardinal. (Contributed by NM, 28-Oct-2003) (Revised by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	cardmin	$$⊢A\in V\to \mathrm{card}\left(\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\right)=\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		numthcor	$$⊢A\in V\to \exists x\in \mathrm{On}A\prec x$$
2		onintrab2	$$⊢\exists x\in \mathrm{On}A\prec x\leftrightarrow \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\in \mathrm{On}$$
3	1 2	sylib	$$⊢A\in V\to \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\in \mathrm{On}$$
4		onelon	$$⊢\left(\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\in \mathrm{On}\wedge y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\right)\to y\in \mathrm{On}$$
5	4	ex	$$⊢\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\in \mathrm{On}\to \left(y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\to y\in \mathrm{On}\right)$$
6	3 5	syl	$$⊢A\in V\to \left(y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\to y\in \mathrm{On}\right)$$
7		breq2	$$⊢x=y\to \left(A\prec x\leftrightarrow A\prec y\right)$$
8	7	onnminsb	$$⊢y\in \mathrm{On}\to \left(y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\to \neg A\prec y\right)$$
9	6 8	syli	$$⊢A\in V\to \left(y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\to \neg A\prec y\right)$$
10		vex	$$⊢y\in \mathrm{V}$$
11		domtri	$$⊢\left(y\in \mathrm{V}\wedge A\in V\right)\to \left(y\preccurlyeq A\leftrightarrow \neg A\prec y\right)$$
12	10 11	mpan	$$⊢A\in V\to \left(y\preccurlyeq A\leftrightarrow \neg A\prec y\right)$$
13	9 12	sylibrd	$$⊢A\in V\to \left(y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\to y\preccurlyeq A\right)$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}x\prec$$
16		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in \mathrm{On}|A\prec x\right\}$$
17	16	nfint	$$⊢\underset{\_}{Ⅎ}x\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}$$
18	14 15 17	nfbr	$$⊢ℲxA\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}$$
19		breq2	$$⊢x=\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\to \left(A\prec x\leftrightarrow A\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\right)$$
20	18 19	onminsb	$$⊢\exists x\in \mathrm{On}A\prec x\to A\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}$$
21	1 20	syl	$$⊢A\in V\to A\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}$$
22	13 21	jctird	$$⊢A\in V\to \left(y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\to \left(y\preccurlyeq A\wedge A\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\right)\right)$$
23		domsdomtr	$$⊢\left(y\preccurlyeq A\wedge A\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\right)\to y\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}$$
24	22 23	syl6	$$⊢A\in V\to \left(y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\to y\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\right)$$
25	24	ralrimiv	$$⊢A\in V\to \forall y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}y\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}$$
26		iscard	$$⊢\mathrm{card}\left(\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\right)=\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\leftrightarrow \left(\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\in \mathrm{On}\wedge \forall y\in \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}y\prec \bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\right)$$
27	3 25 26	sylanbrc	$$⊢A\in V\to \mathrm{card}\left(\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}\right)=\bigcap \left\{x\in \mathrm{On}|A\prec x\right\}$$