fimact

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	$⊢ (A ≼ ω \land Fun F) \to F [A] ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		omelon	$⊢ ω \in On$
2	1	a1i	$⊢ (A ≼ ω \land Fun F) \to ω \in On$
3		simpl	$⊢ (A ≼ ω \land Fun F) \to A ≼ ω$
4		ondomen	$⊢ (ω \in On \land A ≼ ω) \to A \in dom card$
5	2 3 4	syl2anc	$⊢ (A ≼ ω \land Fun F) \to A \in dom card$
6		simpr	$⊢ (A ≼ ω \land Fun F) \to Fun F$
7		imadomnum	$⊢ A \in dom card \to (Fun F \to F [A] ≼ A)$
8	5 6 7	sylc	$⊢ (A ≼ ω \land Fun F) \to F [A] ≼ A$
9		domtr	$⊢ (F [A] ≼ A \land A ≼ ω) \to F [A] ≼ ω$
10	8 3 9	syl2anc	$⊢ (A ≼ ω \land Fun F) \to F [A] ≼ ω$

Metamath Proof Explorer

Theorem fimact

Proof