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

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 ‘ 𝐴 )