Theorem cardval

Description: The value of the cardinal number function. Definition 10.4 of TakeutiZaring p. 85. See cardval2 for a simpler version of its value. (Contributed by NM, 21-Oct-2003) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Hypothesis	cardval.1	|- A e. _V
Assertion	cardval	|- ( card ` A ) = |^| { x e. On | x ~~ A }

Proof

Step	Hyp	Ref	Expression
1		cardval.1	|- A e. _V
2		numth3	|- ( A e. _V -> A e. dom card )
3		cardval3	|- ( A e. dom card -> ( card ` A ) = |^| { x e. On | x ~~ A } )
4	1 2 3	mp2b	|- ( card ` A ) = |^| { x e. On | x ~~ A }