Theorem cardonle

Description: The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of TakeutiZaring p. 85. (Contributed by NM, 22-Oct-2003)

	Ref	Expression
Assertion	cardonle	$$⊢A\in \mathrm{On}\to \mathrm{card}\left(A\right)\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		oncardval	$$⊢A\in \mathrm{On}\to \mathrm{card}\left(A\right)=\bigcap \left\{x\in \mathrm{On}|x\approx A\right\}$$
2		enrefg	$$⊢A\in \mathrm{On}\to A\approx A$$
3		breq1	$$⊢x=A\to \left(x\approx A\leftrightarrow A\approx A\right)$$
4	3	intminss	$$⊢\left(A\in \mathrm{On}\wedge A\approx A\right)\to \bigcap \left\{x\in \mathrm{On}|x\approx A\right\}\subseteq A$$
5	2 4	mpdan	$$⊢A\in \mathrm{On}\to \bigcap \left\{x\in \mathrm{On}|x\approx A\right\}\subseteq A$$
6	1 5	eqsstrd	$$⊢A\in \mathrm{On}\to \mathrm{card}\left(A\right)\subseteq A$$