Description: A set equinumerous to a proper subset of itself is infinite. Corollary 6D(a) of Enderton p. 136. (Contributed by NM, 2-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | pssinf | ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐴 ≈ 𝐵 ) → ¬ 𝐵 ∈ Fin ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | php3 | ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊊ 𝐵 ) → 𝐴 ≺ 𝐵 ) | |
2 | 1 | ex | ⊢ ( 𝐵 ∈ Fin → ( 𝐴 ⊊ 𝐵 → 𝐴 ≺ 𝐵 ) ) |
3 | sdomnen | ⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 ) | |
4 | 2 3 | syl6com | ⊢ ( 𝐴 ⊊ 𝐵 → ( 𝐵 ∈ Fin → ¬ 𝐴 ≈ 𝐵 ) ) |
5 | 4 | con2d | ⊢ ( 𝐴 ⊊ 𝐵 → ( 𝐴 ≈ 𝐵 → ¬ 𝐵 ∈ Fin ) ) |
6 | 5 | imp | ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐴 ≈ 𝐵 ) → ¬ 𝐵 ∈ Fin ) |