Theorem cardidm

Description: The cardinality function is idempotent. Proposition 10.11 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

	Ref	Expression
Assertion	cardidm	|- ( card ` ( card ` A ) ) = ( card ` A )

Proof

Step	Hyp	Ref	Expression
1		cardid2	|- ( A e. dom card -> ( card ` A ) ~~ A )
2	1	ensymd	|- ( A e. dom card -> A ~~ ( card ` A ) )
3		entr	|- ( ( y ~~ A /\ A ~~ ( card ` A ) ) -> y ~~ ( card ` A ) )
4	3	expcom	|- ( A ~~ ( card ` A ) -> ( y ~~ A -> y ~~ ( card ` A ) ) )
5	2 4	syl	|- ( A e. dom card -> ( y ~~ A -> y ~~ ( card ` A ) ) )
6		entr	|- ( ( y ~~ ( card ` A ) /\ ( card ` A ) ~~ A ) -> y ~~ A )
7	6	expcom	|- ( ( card ` A ) ~~ A -> ( y ~~ ( card ` A ) -> y ~~ A ) )
8	1 7	syl	|- ( A e. dom card -> ( y ~~ ( card ` A ) -> y ~~ A ) )
9	5 8	impbid	|- ( A e. dom card -> ( y ~~ A <-> y ~~ ( card ` A ) ) )
10	9	rabbidv	|- ( A e. dom card -> { y e. On | y ~~ A } = { y e. On | y ~~ ( card ` A ) } )
11	10	inteqd	|- ( A e. dom card -> |^| { y e. On | y ~~ A } = |^| { y e. On | y ~~ ( card ` A ) } )
12		cardval3	|- ( A e. dom card -> ( card ` A ) = |^| { y e. On | y ~~ A } )
13		cardon	|- ( card ` A ) e. On
14		oncardval	|- ( ( card ` A ) e. On -> ( card ` ( card ` A ) ) = |^| { y e. On | y ~~ ( card ` A ) } )
15	13 14	mp1i	|- ( A e. dom card -> ( card ` ( card ` A ) ) = |^| { y e. On | y ~~ ( card ` A ) } )
16	11 12 15	3eqtr4rd	|- ( A e. dom card -> ( card ` ( card ` A ) ) = ( card ` A ) )
17		card0	|- ( card ` (/) ) = (/)
18		ndmfv	|- ( -. A e. dom card -> ( card ` A ) = (/) )
19	18	fveq2d	|- ( -. A e. dom card -> ( card ` ( card ` A ) ) = ( card ` (/) ) )
20	17 19 18	3eqtr4a	|- ( -. A e. dom card -> ( card ` ( card ` A ) ) = ( card ` A ) )
21	16 20	pm2.61i	|- ( card ` ( card ` A ) ) = ( card ` A )