Theorem cardidm

Description: The cardinality function is idempotent. Proposition 10.11 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

	Ref	Expression
Assertion	cardidm	$$⊢\mathrm{card}\left(\mathrm{card}\left(A\right)\right)=\mathrm{card}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cardid2	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)\approx A$$
2	1	ensymd	$$⊢A\in \mathrm{dom}\mathrm{card}\to A\approx \mathrm{card}\left(A\right)$$
3		entr	$$⊢\left(y\approx A\wedge A\approx \mathrm{card}\left(A\right)\right)\to y\approx \mathrm{card}\left(A\right)$$
4	3	expcom	$$⊢A\approx \mathrm{card}\left(A\right)\to \left(y\approx A\to y\approx \mathrm{card}\left(A\right)\right)$$
5	2 4	syl	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(y\approx A\to y\approx \mathrm{card}\left(A\right)\right)$$
6		entr	$$⊢\left(y\approx \mathrm{card}\left(A\right)\wedge \mathrm{card}\left(A\right)\approx A\right)\to y\approx A$$
7	6	expcom	$$⊢\mathrm{card}\left(A\right)\approx A\to \left(y\approx \mathrm{card}\left(A\right)\to y\approx A\right)$$
8	1 7	syl	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(y\approx \mathrm{card}\left(A\right)\to y\approx A\right)$$
9	5 8	impbid	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(y\approx A\leftrightarrow y\approx \mathrm{card}\left(A\right)\right)$$
10	9	rabbidv	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left\{y\in \mathrm{On}|y\approx A\right\}=\left\{y\in \mathrm{On}|y\approx \mathrm{card}\left(A\right)\right\}$$
11	10	inteqd	$$⊢A\in \mathrm{dom}\mathrm{card}\to \bigcap \left\{y\in \mathrm{On}|y\approx A\right\}=\bigcap \left\{y\in \mathrm{On}|y\approx \mathrm{card}\left(A\right)\right\}$$
12		cardval3	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)=\bigcap \left\{y\in \mathrm{On}|y\approx A\right\}$$
13		cardon	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}$$
14		oncardval	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}\to \mathrm{card}\left(\mathrm{card}\left(A\right)\right)=\bigcap \left\{y\in \mathrm{On}|y\approx \mathrm{card}\left(A\right)\right\}$$
15	13 14	mp1i	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(\mathrm{card}\left(A\right)\right)=\bigcap \left\{y\in \mathrm{On}|y\approx \mathrm{card}\left(A\right)\right\}$$
16	11 12 15	3eqtr4rd	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(\mathrm{card}\left(A\right)\right)=\mathrm{card}\left(A\right)$$
17		card0	$$⊢\mathrm{card}\left(\varnothing \right)=\varnothing$$
18		ndmfv	$$⊢\neg A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)=\varnothing$$
19	18	fveq2d	$$⊢\neg A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(\mathrm{card}\left(A\right)\right)=\mathrm{card}\left(\varnothing \right)$$
20	17 19 18	3eqtr4a	$$⊢\neg A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(\mathrm{card}\left(A\right)\right)=\mathrm{card}\left(A\right)$$
21	16 20	pm2.61i	$$⊢\mathrm{card}\left(\mathrm{card}\left(A\right)\right)=\mathrm{card}\left(A\right)$$