Description: The image by a function of a countable set is countable. The proof uses imadomnum rather than imadomg , and so does not require ax-ac . (Contributed by Thierry Arnoux, 27-Mar-2018) (Revised by Vincent Gonzalez, 25-Aug-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fimact | ⊢ ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → ( 𝐹 “ 𝐴 ) ≼ ω ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | omelon | ⊢ ω ∈ On | |
| 2 | 1 | a1i | ⊢ ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → ω ∈ On ) |
| 3 | simpl | ⊢ ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → 𝐴 ≼ ω ) | |
| 4 | ondomen | ⊢ ( ( ω ∈ On ∧ 𝐴 ≼ ω ) → 𝐴 ∈ dom card ) | |
| 5 | 2 3 4 | syl2anc | ⊢ ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → 𝐴 ∈ dom card ) |
| 6 | simpr | ⊢ ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → Fun 𝐹 ) | |
| 7 | imadomnum | ⊢ ( 𝐴 ∈ dom card → ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) ) | |
| 8 | 5 6 7 | sylc | ⊢ ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) |
| 9 | domtr | ⊢ ( ( ( 𝐹 “ 𝐴 ) ≼ 𝐴 ∧ 𝐴 ≼ ω ) → ( 𝐹 “ 𝐴 ) ≼ ω ) | |
| 10 | 8 3 9 | syl2anc | ⊢ ( ( 𝐴 ≼ ω ∧ Fun 𝐹 ) → ( 𝐹 “ 𝐴 ) ≼ ω ) |