fnct

Description: If the domain of a function is countable, the function is countable. The proof uses fnrndomnum rather than fnrndomg , and so does not require ax-ac . (Contributed by Thierry Arnoux, 29-Dec-2016) (Revised by Vincent Gonzalez, 24-Aug-2026)

		Ref	Expression
	Assertion	fnct	$⊢ (F Fn A \land A ≼ ω) \to F ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		ctex	$⊢ A ≼ ω \to A \in V$
2	1	adantl	$⊢ (F Fn A \land A ≼ ω) \to A \in V$
3		fndm	$⊢ F Fn A \to dom F = A$
4	3	eleq1d	$⊢ F Fn A \to (dom F \in V \leftrightarrow A \in V)$
5	4	adantr	$⊢ (F Fn A \land A ≼ ω) \to (dom F \in V \leftrightarrow A \in V)$
6	2 5	mpbird	$⊢ (F Fn A \land A ≼ ω) \to dom F \in V$
7		fnfun	$⊢ F Fn A \to Fun F$
8	7	adantr	$⊢ (F Fn A \land A ≼ ω) \to Fun F$
9		funrnex	$⊢ dom F \in V \to (Fun F \to ran F \in V)$
10	6 8 9	sylc	$⊢ (F Fn A \land A ≼ ω) \to ran F \in V$
11	2 10	xpexd	$⊢ (F Fn A \land A ≼ ω) \to A \times ran F \in V$
12		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
13	12	birani	$⊢ (F Fn A \land A ≼ ω) \to F : A ⟶ ran F$
14		fssxp	$⊢ F : A ⟶ ran F \to F \subseteq A \times ran F$
15	13 14	syl	$⊢ (F Fn A \land A ≼ ω) \to F \subseteq A \times ran F$
16		ssdomg	$⊢ A \times ran F \in V \to (F \subseteq A \times ran F \to F ≼ (A \times ran F))$
17	11 15 16	sylc	$⊢ (F Fn A \land A ≼ ω) \to F ≼ (A \times ran F)$
18		xpdom1g	$⊢ (ran F \in V \land A ≼ ω) \to (A \times ran F) ≼ (ω \times ran F)$
19	10 18	sylancom	$⊢ (F Fn A \land A ≼ ω) \to (A \times ran F) ≼ (ω \times ran F)$
20		omex	$⊢ ω \in V$
21		omelon	$⊢ ω \in On$
22	21	a1i	$⊢ (F Fn A \land A ≼ ω) \to ω \in On$
23		simpr	$⊢ (F Fn A \land A ≼ ω) \to A ≼ ω$
24		ondomen	$⊢ (ω \in On \land A ≼ ω) \to A \in dom card$
25	22 23 24	syl2anc	$⊢ (F Fn A \land A ≼ ω) \to A \in dom card$
26		simpl	$⊢ (F Fn A \land A ≼ ω) \to F Fn A$
27		fnrndomnum	$⊢ A \in dom card \to (F Fn A \to ran F ≼ A)$
28	25 26 27	sylc	$⊢ (F Fn A \land A ≼ ω) \to ran F ≼ A$
29		domtr	$⊢ (ran F ≼ A \land A ≼ ω) \to ran F ≼ ω$
30	28 29	sylancom	$⊢ (F Fn A \land A ≼ ω) \to ran F ≼ ω$
31		xpdom2g	$⊢ (ω \in V \land ran F ≼ ω) \to (ω \times ran F) ≼ (ω \times ω)$
32	20 30 31	sylancr	$⊢ (F Fn A \land A ≼ ω) \to (ω \times ran F) ≼ (ω \times ω)$
33		domtr	$⊢ ((A \times ran F) ≼ (ω \times ran F) \land (ω \times ran F) ≼ (ω \times ω)) \to (A \times ran F) ≼ (ω \times ω)$
34	19 32 33	syl2anc	$⊢ (F Fn A \land A ≼ ω) \to (A \times ran F) ≼ (ω \times ω)$
35		xpomen	$⊢ (ω \times ω) \approx ω$
36		domentr	$⊢ ((A \times ran F) ≼ (ω \times ω) \land (ω \times ω) \approx ω) \to (A \times ran F) ≼ ω$
37	34 35 36	sylancl	$⊢ (F Fn A \land A ≼ ω) \to (A \times ran F) ≼ ω$
38		domtr	$⊢ (F ≼ (A \times ran F) \land (A \times ran F) ≼ ω) \to F ≼ ω$
39	17 37 38	syl2anc	$⊢ (F Fn A \land A ≼ ω) \to F ≼ ω$

Metamath Proof Explorer

Theorem fnct

Proof