Description: A set is finite iff it is strictly dominated by the class of natural number. Theorem 42 of Suppes p. 151. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 3-Nov-2002) (Revised by Mario Carneiro, 27-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | isfiniteg | ⊢ ( ω ∈ V → ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isfi | ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ) | |
| 2 | nnsdomg | ⊢ ( ( ω ∈ V ∧ 𝑥 ∈ ω ) → 𝑥 ≺ ω ) | |
| 3 | sdomen1 | ⊢ ( 𝐴 ≈ 𝑥 → ( 𝐴 ≺ ω ↔ 𝑥 ≺ ω ) ) | |
| 4 | 2 3 | syl5ibrcom | ⊢ ( ( ω ∈ V ∧ 𝑥 ∈ ω ) → ( 𝐴 ≈ 𝑥 → 𝐴 ≺ ω ) ) |
| 5 | 4 | rexlimdva | ⊢ ( ω ∈ V → ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → 𝐴 ≺ ω ) ) |
| 6 | 1 5 | syl5bi | ⊢ ( ω ∈ V → ( 𝐴 ∈ Fin → 𝐴 ≺ ω ) ) |
| 7 | isfinite2 | ⊢ ( 𝐴 ≺ ω → 𝐴 ∈ Fin ) | |
| 8 | 6 7 | impbid1 | ⊢ ( ω ∈ V → ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω ) ) |