Metamath Proof Explorer

Theorem 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 ∧ A ≼ ω → F ≼ ω

Proof

Step Hyp Ref Expression
1 ctex ⊢ A ≼ ω → A ∈ V
2 1 adantl ⊢ F Fn A ∧ A ≼ ω → A ∈ V
3 fndm ⊢ F Fn A → dom ⁡ F = A
4 3 eleq1d ⊢ F Fn A → dom ⁡ F ∈ V ↔ A ∈ V
5 4 adantr ⊢ F Fn A ∧ A ≼ ω → dom ⁡ F ∈ V ↔ A ∈ V
6 2 5 mpbird ⊢ F Fn A ∧ A ≼ ω → dom ⁡ F ∈ V
7 fnfun ⊢ F Fn A → Fun ⁡ F
8 7 adantr ⊢ F Fn A ∧ A ≼ ω → Fun ⁡ F
9 funrnex ⊢ dom ⁡ F ∈ V → Fun ⁡ F → ran ⁡ F ∈ V
10 6 8 9 sylc ⊢ F Fn A ∧ A ≼ ω → ran ⁡ F ∈ V
11 2 10 xpexd ⊢ F Fn A ∧ A ≼ ω → A × ran ⁡ F ∈ V
12 simpl ⊢ F Fn A ∧ A ≼ ω → F Fn A
13 dffn3 ⊢ F Fn A ↔ F : A ⟶ ran ⁡ F
14 12 13 sylib ⊢ F Fn A ∧ A ≼ ω → F : A ⟶ ran ⁡ F
15 fssxp ⊢ F : A ⟶ ran ⁡ F → F ⊆ A × ran ⁡ F
16 14 15 syl ⊢ F Fn A ∧ A ≼ ω → F ⊆ A × ran ⁡ F
17 ssdomg ⊢ A × ran ⁡ F ∈ V → F ⊆ A × ran ⁡ F → F ≼ A × ran ⁡ F
18 11 16 17 sylc ⊢ F Fn A ∧ A ≼ ω → F ≼ A × ran ⁡ F
19 xpdom1g ⊢ ran ⁡ F ∈ V ∧ A ≼ ω → A × ran ⁡ F ≼ ω × ran ⁡ F
20 10 19 sylancom ⊢ F Fn A ∧ A ≼ ω → A × ran ⁡ F ≼ ω × ran ⁡ F
21 omex ⊢ ω ∈ V
22 fnrndomg ⊢ A ∈ V → F Fn A → ran ⁡ F ≼ A
23 2 12 22 sylc ⊢ F Fn A ∧ A ≼ ω → ran ⁡ F ≼ A
24 domtr ⊢ ran ⁡ F ≼ A ∧ A ≼ ω → ran ⁡ F ≼ ω
25 23 24 sylancom ⊢ F Fn A ∧ A ≼ ω → ran ⁡ F ≼ ω
26 xpdom2g ⊢ ω ∈ V ∧ ran ⁡ F ≼ ω → ω × ran ⁡ F ≼ ω × ω
27 21 25 26 sylancr ⊢ F Fn A ∧ A ≼ ω → ω × ran ⁡ F ≼ ω × ω
28 domtr ⊢ A × ran ⁡ F ≼ ω × ran ⁡ F ∧ ω × ran ⁡ F ≼ ω × ω → A × ran ⁡ F ≼ ω × ω
29 20 27 28 syl2anc ⊢ F Fn A ∧ A ≼ ω → A × ran ⁡ F ≼ ω × ω
30 xpomen ⊢ ω × ω ≈ ω
31 domentr ⊢ A × ran ⁡ F ≼ ω × ω ∧ ω × ω ≈ ω → A × ran ⁡ F ≼ ω
32 29 30 31 sylancl ⊢ F Fn A ∧ A ≼ ω → A × ran ⁡ F ≼ ω
33 domtr ⊢ F ≼ A × ran ⁡ F ∧ A × ran ⁡ F ≼ ω → F ≼ ω
34 18 32 33 syl2anc ⊢ F Fn A ∧ A ≼ ω → F ≼ ω