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 ⊢ A ≈ B → A = B

Proof

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