Theorem 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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → 𝐹 ≼ ω )

Proof

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