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↔∃xx∈ω∧B≈x
3 1 2 sylbb ⊢B∈Fin→∃xx∈ω∧B≈x
4 ensymfib ⊢B∈Fin→B≈A↔A≈B
5 4 biimparc ⊢A≈B∧B∈Fin→B≈A
6 19.41v ⊢∃xx∈ω∧B≈x∧B≈A↔∃xx∈ω∧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 ⊢∃xx∈ω∧B≈x∧B≈A→∃xx∈ω∧A≈x
21 6 20 sylbir ⊢∃xx∈ω∧B≈x∧B≈A→∃xx∈ω∧A≈x
22 3 5 21 syl2an2 ⊢A≈B∧B∈Fin→∃xx∈ω∧A≈x
23 df-rex ⊢∃x∈ωA≈x↔∃xx∈ω∧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