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 e. On -> ( card ` A ) C_ A )

Proof

Step	Hyp	Ref	Expression
1		oncardval	|- ( A e. On -> ( card ` A ) = |^| { x e. On | x ~~ A } )
2		enrefg	|- ( A e. On -> A ~~ A )
3		breq1	|- ( x = A -> ( x ~~ A <-> A ~~ A ) )
4	3	intminss	|- ( ( A e. On /\ A ~~ A ) -> |^| { x e. On | x ~~ A } C_ A )
5	2 4	mpdan	|- ( A e. On -> |^| { x e. On | x ~~ A } C_ A )
6	1 5	eqsstrd	|- ( A e. On -> ( card ` A ) C_ A )