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

Metamath Proof Explorer

Theorem hasheni

Description: Equinumerous sets have the same number of elements (even if they are not finite). (Contributed by Mario Carneiro, 15-Apr-2015)

Ref Expression
Assertion hasheni ( 𝐴 ≈ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐴 ≈ 𝐵 )
2 enfii ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ∈ Fin )
3 2 ancoms ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → 𝐴 ∈ Fin )
4 hashen ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
5 3 4 sylancom ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
6 1 5 mpbird ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
7 relen ⊢ Rel ≈
8 7 brrelex1i ⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
9 enfi ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )
10 9 notbid ⊢ ( 𝐴 ≈ 𝐵 → ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝐵 ∈ Fin ) )
11 10 biimpar ⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐵 ∈ Fin ) → ¬ 𝐴 ∈ Fin )
12 hashinf ⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
13 8 11 12 syl2an2r ⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
14 7 brrelex2i ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
15 hashinf ⊢ ( ( 𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
16 14 15 sylan ⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
17 13 16 eqtr4d ⊢ ( ( 𝐴 ≈ 𝐵 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
18 6 17 pm2.61dan ⊢ ( 𝐴 ≈ 𝐵 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )