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