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 
|- ( ( 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 )