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 ‘ 𝐴 ) ) = ( card ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 cardid2 ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
2 1 ensymd ( 𝐴 ∈ dom card → 𝐴 ≈ ( card ‘ 𝐴 ) )
3 entr ( ( 𝑦𝐴𝐴 ≈ ( card ‘ 𝐴 ) ) → 𝑦 ≈ ( card ‘ 𝐴 ) )
4 3 expcom ( 𝐴 ≈ ( card ‘ 𝐴 ) → ( 𝑦𝐴𝑦 ≈ ( card ‘ 𝐴 ) ) )
5 2 4 syl ( 𝐴 ∈ dom card → ( 𝑦𝐴𝑦 ≈ ( card ‘ 𝐴 ) ) )
6 entr ( ( 𝑦 ≈ ( card ‘ 𝐴 ) ∧ ( card ‘ 𝐴 ) ≈ 𝐴 ) → 𝑦𝐴 )
7 6 expcom ( ( card ‘ 𝐴 ) ≈ 𝐴 → ( 𝑦 ≈ ( card ‘ 𝐴 ) → 𝑦𝐴 ) )
8 1 7 syl ( 𝐴 ∈ dom card → ( 𝑦 ≈ ( card ‘ 𝐴 ) → 𝑦𝐴 ) )
9 5 8 impbid ( 𝐴 ∈ dom card → ( 𝑦𝐴𝑦 ≈ ( card ‘ 𝐴 ) ) )
10 9 rabbidv ( 𝐴 ∈ dom card → { 𝑦 ∈ On ∣ 𝑦𝐴 } = { 𝑦 ∈ On ∣ 𝑦 ≈ ( card ‘ 𝐴 ) } )
11 10 inteqd ( 𝐴 ∈ dom card → { 𝑦 ∈ On ∣ 𝑦𝐴 } = { 𝑦 ∈ On ∣ 𝑦 ≈ ( card ‘ 𝐴 ) } )
12 cardval3 ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = { 𝑦 ∈ On ∣ 𝑦𝐴 } )
13 cardon ( card ‘ 𝐴 ) ∈ On
14 oncardval ( ( card ‘ 𝐴 ) ∈ On → ( card ‘ ( card ‘ 𝐴 ) ) = { 𝑦 ∈ On ∣ 𝑦 ≈ ( card ‘ 𝐴 ) } )
15 13 14 mp1i ( 𝐴 ∈ dom card → ( card ‘ ( card ‘ 𝐴 ) ) = { 𝑦 ∈ On ∣ 𝑦 ≈ ( card ‘ 𝐴 ) } )
16 11 12 15 3eqtr4rd ( 𝐴 ∈ dom card → ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) )
17 card0 ( card ‘ ∅ ) = ∅
18 ndmfv ( ¬ 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∅ )
19 18 fveq2d ( ¬ 𝐴 ∈ dom card → ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ ∅ ) )
20 17 19 18 3eqtr4a ( ¬ 𝐴 ∈ dom card → ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) )
21 16 20 pm2.61i ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 )