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 | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ensymfib | ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴 ) ) | |
| 2 | 1 | pm5.32i | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ↔ ( 𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴 ) ) |
| 3 | enfii | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴 ) → 𝐵 ∈ Fin ) | |
| 4 | 2 3 | sylbi | ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐵 ∈ Fin ) |
| 5 | 4 | expcom | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin → 𝐵 ∈ Fin ) ) |
| 6 | enfii | ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ∈ Fin ) | |
| 7 | 6 | expcom | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐵 ∈ Fin → 𝐴 ∈ Fin ) ) |
| 8 | 5 7 | impbid | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) ) |