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 + 1 0 ↾ ω ⁡ card ⁡ card ⁡ A = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ 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 + 1 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
8 7 hashgval ⊢ card ⁡ A ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ card ⁡ A = card ⁡ A
9 6 8 syl ⊢ A ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ card ⁡ A = card ⁡ A
10 7 hashgval ⊢ A ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ A = A
11 2 9 10 3eqtr3a ⊢ A ∈ Fin → card ⁡ A = A