Metamath Proof Explorer

Theorem enfii

Description: A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015) Avoid ax-pow . (Revised by BTernaryTau, 23-Sep-2024)

Ref Expression
Assertion enfii ⊢ B ∈ Fin ∧ A ≈ B → A ∈ Fin

Proof

Step Hyp Ref Expression
1 isfi ⊢ B ∈ Fin ↔ ∃ x ∈ ω B ≈ x
2 df-rex ⊢ ∃ x ∈ ω B ≈ x ↔ ∃ x x ∈ ω ∧ B ≈ x
3 1 2 sylbb ⊢ B ∈ Fin → ∃ x x ∈ ω ∧ B ≈ x
4 ensymfib ⊢ B ∈ Fin → B ≈ A ↔ A ≈ B
5 4 biimparc ⊢ A ≈ B ∧ B ∈ Fin → B ≈ A
6 19.41v ⊢ ∃ x x ∈ ω ∧ B ≈ x ∧ B ≈ A ↔ ∃ x x ∈ ω ∧ B ≈ x ∧ B ≈ A
7 simp1 ⊢ x ∈ ω ∧ B ≈ x ∧ B ≈ A → x ∈ ω
8 nnfi ⊢ x ∈ ω → x ∈ Fin
9 ensymfib ⊢ x ∈ Fin → x ≈ B ↔ B ≈ x
10 9 biimpar ⊢ x ∈ Fin ∧ B ≈ x → x ≈ B
11 10 3adant3 ⊢ x ∈ Fin ∧ B ≈ x ∧ B ≈ A → x ≈ B
12 entrfil ⊢ x ∈ Fin ∧ x ≈ B ∧ B ≈ A → x ≈ A
13 11 12 syld3an2 ⊢ x ∈ Fin ∧ B ≈ x ∧ B ≈ A → x ≈ A
14 ensymfib ⊢ x ∈ Fin → x ≈ A ↔ A ≈ x
15 14 3ad2ant1 ⊢ x ∈ Fin ∧ B ≈ x ∧ B ≈ A → x ≈ A ↔ A ≈ x
16 13 15 mpbid ⊢ x ∈ Fin ∧ B ≈ x ∧ B ≈ A → A ≈ x
17 8 16 syl3an1 ⊢ x ∈ ω ∧ B ≈ x ∧ B ≈ A → A ≈ x
18 7 17 jca ⊢ x ∈ ω ∧ B ≈ x ∧ B ≈ A → x ∈ ω ∧ A ≈ x
19 18 3expa ⊢ x ∈ ω ∧ B ≈ x ∧ B ≈ A → x ∈ ω ∧ A ≈ x
20 19 eximi ⊢ ∃ x x ∈ ω ∧ B ≈ x ∧ B ≈ A → ∃ x x ∈ ω ∧ A ≈ x
21 6 20 sylbir ⊢ ∃ x x ∈ ω ∧ B ≈ x ∧ B ≈ A → ∃ x x ∈ ω ∧ A ≈ x
22 3 5 21 syl2an2 ⊢ A ≈ B ∧ B ∈ Fin → ∃ x x ∈ ω ∧ A ≈ x
23 df-rex ⊢ ∃ x ∈ ω A ≈ x ↔ ∃ x x ∈ ω ∧ A ≈ x
24 22 23 sylibr ⊢ A ≈ B ∧ B ∈ Fin → ∃ x ∈ ω A ≈ x
25 isfi ⊢ A ∈ Fin ↔ ∃ x ∈ ω A ≈ x
26 24 25 sylibr ⊢ A ≈ B ∧ B ∈ Fin → A ∈ Fin
27 26 ancoms ⊢ B ∈ Fin ∧ A ≈ B → A ∈ Fin