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

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 ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ∈ Fin )

Proof

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