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

Metamath Proof Explorer

Theorem cardval3

Description: An alternate definition of the value of ( cardA ) that does not require AC to prove. (Contributed by Mario Carneiro, 7-Jan-2013) (Revised by Mario Carneiro, 27-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. dom card -> A e. _V )
2 isnum2 
 |-  ( A e. dom card <-> E. x e. On x ~~ A )
3 rabn0 
 |-  ( { x e. On | x ~~ A } =/= (/) <-> E. x e. On x ~~ A )
4 intex 
 |-  ( { x e. On | x ~~ A } =/= (/) <-> |^| { x e. On | x ~~ A } e. _V )
5 2 3 4 3bitr2i 
 |-  ( A e. dom card <-> |^| { x e. On | x ~~ A } e. _V )
6 5 biimpi 
 |-  ( A e. dom card -> |^| { x e. On | x ~~ A } e. _V )
7 breq2 
 |-  ( y = A -> ( x ~~ y <-> x ~~ A ) )
8 7 rabbidv 
 |-  ( y = A -> { x e. On | x ~~ y } = { x e. On | x ~~ A } )
9 8 inteqd 
 |-  ( y = A -> |^| { x e. On | x ~~ y } = |^| { x e. On | x ~~ A } )
10 df-card 
 |-  card = ( y e. _V |-> |^| { x e. On | x ~~ y } )
11 9 10 fvmptg 
 |-  ( ( A e. _V /\ |^| { x e. On | x ~~ A } e. _V ) -> ( card ` A ) = |^| { x e. On | x ~~ A } )
12 1 6 11 syl2anc 
 |-  ( A e. dom card -> ( card ` A ) = |^| { x e. On | x ~~ A } )