Metamath Proof Explorer

Theorem hashen

Description: Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion hashen ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ♯ ‘ 𝐵 ) ) )
2 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
3 2 hashginv ⊢ ( 𝐴 ∈ Fin → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ♯ ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) )
4 2 hashginv ⊢ ( 𝐵 ∈ Fin → ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ♯ ‘ 𝐵 ) ) = ( card ‘ 𝐵 ) )
5 3 4 eqeqan12d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ◡ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( ♯ ‘ 𝐵 ) ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )
6 1 5 imbitrid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) → ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )
7 fveq2 ⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) )
8 2 hashgval ⊢ ( 𝐴 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )
9 2 hashgval ⊢ ( 𝐵 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) = ( ♯ ‘ 𝐵 ) )
10 8 9 eqeqan12d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐵 ) ) ↔ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
11 7 10 imbitrid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ) )
12 6 11 impbid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )
13 finnum ⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )
14 finnum ⊢ ( 𝐵 ∈ Fin → 𝐵 ∈ dom card )
15 carden2 ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
16 13 14 15 syl2an ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
17 12 16 bitrd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )