Metamath Proof Explorer

Theorem hashcard

Description: The size function of the cardinality function. (Contributed by Mario Carneiro, 19-Sep-2013) (Revised by Mario Carneiro, 4-Nov-2013)

Ref Expression
Assertion hashcard ( 𝐴 ∈ Fin → ( ♯ ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cardidm ⊢ ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 )
2 1 fveq2i ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( card ‘ 𝐴 ) ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) )
3 ficardom ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )
4 ssid ⊢ ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐴 )
5 ssnnfi ⊢ ( ( ( card ‘ 𝐴 ) ∈ ω ∧ ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐴 ) ) → ( card ‘ 𝐴 ) ∈ Fin )
6 3 4 5 sylancl ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ Fin )
7 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
8 7 hashgval ⊢ ( ( card ‘ 𝐴 ) ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( card ‘ 𝐴 ) ) ) = ( ♯ ‘ ( card ‘ 𝐴 ) ) )
9 6 8 syl ⊢ ( 𝐴 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ ( card ‘ 𝐴 ) ) ) = ( ♯ ‘ ( card ‘ 𝐴 ) ) )
10 7 hashgval ⊢ ( 𝐴 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )
11 2 9 10 3eqtr3a ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )