This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )