Theorem cardval2

Description: An alternate version of the value of the cardinal number of a set. Compare cardval . This theorem could be used to give a simpler definition of card in place of df-card . It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003)

	Ref	Expression
Assertion	cardval2	|- ( A e. dom card -> ( card ` A ) = { x e. On | x ~< A } )

Proof

Step	Hyp	Ref	Expression
1		cardon	|- ( card ` A ) e. On
2	1	oneli	|- ( x e. ( card ` A ) -> x e. On )
3	2	pm4.71ri	|- ( x e. ( card ` A ) <-> ( x e. On /\ x e. ( card ` A ) ) )
4		cardsdomel	|- ( ( x e. On /\ A e. dom card ) -> ( x ~< A <-> x e. ( card ` A ) ) )
5	4	ancoms	|- ( ( A e. dom card /\ x e. On ) -> ( x ~< A <-> x e. ( card ` A ) ) )
6	5	pm5.32da	|- ( A e. dom card -> ( ( x e. On /\ x ~< A ) <-> ( x e. On /\ x e. ( card ` A ) ) ) )
7	3 6	bitr4id	|- ( A e. dom card -> ( x e. ( card ` A ) <-> ( x e. On /\ x ~< A ) ) )
8	7	eqabdv	|- ( A e. dom card -> ( card ` A ) = { x | ( x e. On /\ x ~< A ) } )
9		df-rab	|- { x e. On | x ~< A } = { x | ( x e. On /\ x ~< A ) }
10	8 9	eqtr4di	|- ( A e. dom card -> ( card ` A ) = { x e. On | x ~< A } )