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 )