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 ⊢A∈Fin→card⁡A=A

Proof

Step Hyp Ref Expression
1 cardidm ⊢card⁡card⁡A=card⁡A
2 1 fveq2i ⊢rec⁡x∈V⟼x+10↾ω⁡card⁡card⁡A=rec⁡x∈V⟼x+10↾ω⁡card⁡A
3 ficardom ⊢A∈Fin→card⁡A∈ω
4 ssid ⊢card⁡A⊆card⁡A
5 ssnnfi ⊢card⁡A∈ω∧card⁡A⊆card⁡A→card⁡A∈Fin
6 3 4 5 sylancl ⊢A∈Fin→card⁡A∈Fin
7 eqid ⊢rec⁡x∈V⟼x+10↾ω=rec⁡x∈V⟼x+10↾ω
8 7 hashgval ⊢card⁡A∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡card⁡A=card⁡A
9 6 8 syl ⊢A∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡card⁡A=card⁡A
10 7 hashgval ⊢A∈Fin→rec⁡x∈V⟼x+10↾ω⁡card⁡A=A
11 2 9 10 3eqtr3a ⊢A∈Fin→card⁡A=A