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 e. Fin /\ A ~~ B ) -> A e. Fin )

Proof

Step	Hyp	Ref	Expression
1		isfi	|- ( B e. Fin <-> E. x e. _om B ~~ x )
2		df-rex	|- ( E. x e. _om B ~~ x <-> E. x ( x e. _om /\ B ~~ x ) )
3	1 2	sylbb	|- ( B e. Fin -> E. x ( x e. _om /\ B ~~ x ) )
4		ensymfib	|- ( B e. Fin -> ( B ~~ A <-> A ~~ B ) )
5	4	biimparc	|- ( ( A ~~ B /\ B e. Fin ) -> B ~~ A )
6		19.41v	|- ( E. x ( ( x e. _om /\ B ~~ x ) /\ B ~~ A ) <-> ( E. x ( x e. _om /\ B ~~ x ) /\ B ~~ A ) )
7		simp1	|- ( ( x e. _om /\ B ~~ x /\ B ~~ A ) -> x e. _om )
8		nnfi	|- ( x e. _om -> x e. Fin )
9		ensymfib	|- ( x e. Fin -> ( x ~~ B <-> B ~~ x ) )
10	9	biimpar	|- ( ( x e. Fin /\ B ~~ x ) -> x ~~ B )
11	10	3adant3	|- ( ( x e. Fin /\ B ~~ x /\ B ~~ A ) -> x ~~ B )
12		entrfil	|- ( ( x e. Fin /\ x ~~ B /\ B ~~ A ) -> x ~~ A )
13	11 12	syld3an2	|- ( ( x e. Fin /\ B ~~ x /\ B ~~ A ) -> x ~~ A )
14		ensymfib	|- ( x e. Fin -> ( x ~~ A <-> A ~~ x ) )
15	14	3ad2ant1	|- ( ( x e. Fin /\ B ~~ x /\ B ~~ A ) -> ( x ~~ A <-> A ~~ x ) )
16	13 15	mpbid	|- ( ( x e. Fin /\ B ~~ x /\ B ~~ A ) -> A ~~ x )
17	8 16	syl3an1	|- ( ( x e. _om /\ B ~~ x /\ B ~~ A ) -> A ~~ x )
18	7 17	jca	|- ( ( x e. _om /\ B ~~ x /\ B ~~ A ) -> ( x e. _om /\ A ~~ x ) )
19	18	3expa	|- ( ( ( x e. _om /\ B ~~ x ) /\ B ~~ A ) -> ( x e. _om /\ A ~~ x ) )
20	19	eximi	|- ( E. x ( ( x e. _om /\ B ~~ x ) /\ B ~~ A ) -> E. x ( x e. _om /\ A ~~ x ) )
21	6 20	sylbir	|- ( ( E. x ( x e. _om /\ B ~~ x ) /\ B ~~ A ) -> E. x ( x e. _om /\ A ~~ x ) )
22	3 5 21	syl2an2	|- ( ( A ~~ B /\ B e. Fin ) -> E. x ( x e. _om /\ A ~~ x ) )
23		df-rex	|- ( E. x e. _om A ~~ x <-> E. x ( x e. _om /\ A ~~ x ) )
24	22 23	sylibr	|- ( ( A ~~ B /\ B e. Fin ) -> E. x e. _om A ~~ x )
25		isfi	|- ( A e. Fin <-> E. x e. _om A ~~ x )
26	24 25	sylibr	|- ( ( A ~~ B /\ B e. Fin ) -> A e. Fin )
27	26	ancoms	|- ( ( B e. Fin /\ A ~~ B ) -> A e. Fin )