Description: Equinumerous sets have the same finiteness. For a shorter proof using ax-pow , see enfiALT . (Contributed by NM, 22-Aug-2008) Avoid ax-pow . (Revised by BTernaryTau, 23-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | enfi | |- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ensymfib | |- ( A e. Fin -> ( A ~~ B <-> B ~~ A ) ) |
|
| 2 | 1 | pm5.32i | |- ( ( A e. Fin /\ A ~~ B ) <-> ( A e. Fin /\ B ~~ A ) ) |
| 3 | enfii | |- ( ( A e. Fin /\ B ~~ A ) -> B e. Fin ) |
|
| 4 | 2 3 | sylbi | |- ( ( A e. Fin /\ A ~~ B ) -> B e. Fin ) |
| 5 | 4 | expcom | |- ( A ~~ B -> ( A e. Fin -> B e. Fin ) ) |
| 6 | enfii | |- ( ( B e. Fin /\ A ~~ B ) -> A e. Fin ) |
|
| 7 | 6 | expcom | |- ( A ~~ B -> ( B e. Fin -> A e. Fin ) ) |
| 8 | 5 7 | impbid | |- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) ) |