fnct

Description: If the domain of a function is countable, the function is countable. (Contributed by Thierry Arnoux, 29-Dec-2016)

		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		simpl	$⊢ (F Fn A \land A ≼ ω) \to F Fn A$
13		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
14	12 13	sylib	$⊢ (F Fn A \land A ≼ ω) \to F : A ⟶ ran F$
15		fssxp	$⊢ F : A ⟶ ran F \to F \subseteq A \times ran F$
16	14 15	syl	$⊢ (F Fn A \land A ≼ ω) \to F \subseteq A \times ran F$
17		ssdomg	$⊢ A \times ran F \in V \to (F \subseteq A \times ran F \to F ≼ (A \times ran F))$
18	11 16 17	sylc	$⊢ (F Fn A \land A ≼ ω) \to F ≼ (A \times ran F)$
19		xpdom1g	$⊢ (ran F \in V \land A ≼ ω) \to (A \times ran F) ≼ (ω \times ran F)$
20	10 19	sylancom	$⊢ (F Fn A \land A ≼ ω) \to (A \times ran F) ≼ (ω \times ran F)$
21		omex	$⊢ ω \in V$
22		fnrndomg	$⊢ A \in V \to (F Fn A \to ran F ≼ A)$
23	2 12 22	sylc	$⊢ (F Fn A \land A ≼ ω) \to ran F ≼ A$
24		domtr	$⊢ (ran F ≼ A \land A ≼ ω) \to ran F ≼ ω$
25	23 24	sylancom	$⊢ (F Fn A \land A ≼ ω) \to ran F ≼ ω$
26		xpdom2g	$⊢ (ω \in V \land ran F ≼ ω) \to (ω \times ran F) ≼ (ω \times ω)$
27	21 25 26	sylancr	$⊢ (F Fn A \land A ≼ ω) \to (ω \times ran F) ≼ (ω \times ω)$
28		domtr	$⊢ ((A \times ran F) ≼ (ω \times ran F) \land (ω \times ran F) ≼ (ω \times ω)) \to (A \times ran F) ≼ (ω \times ω)$
29	20 27 28	syl2anc	$⊢ (F Fn A \land A ≼ ω) \to (A \times ran F) ≼ (ω \times ω)$
30		xpomen	$⊢ (ω \times ω) \approx ω$
31		domentr	$⊢ ((A \times ran F) ≼ (ω \times ω) \land (ω \times ω) \approx ω) \to (A \times ran F) ≼ ω$
32	29 30 31	sylancl	$⊢ (F Fn A \land A ≼ ω) \to (A \times ran F) ≼ ω$
33		domtr	$⊢ (F ≼ (A \times ran F) \land (A \times ran F) ≼ ω) \to F ≼ ω$
34	18 32 33	syl2anc	$⊢ (F Fn A \land A ≼ ω) \to F ≼ ω$

Metamath Proof Explorer

Theorem fnct

Proof