Metamath Proof Explorer


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 )