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 ( ( 𝐹 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 simpl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → 𝐹 Fn 𝐴 )
13 dffn3 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
14 12 13 sylib ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → 𝐹 : 𝐴 ⟶ ran 𝐹 )
15 fssxp ⊢ ( 𝐹 : 𝐴 ⟶ ran 𝐹 → 𝐹 ⊆ ( 𝐴 × ran 𝐹 ) )
16 14 15 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → 𝐹 ⊆ ( 𝐴 × ran 𝐹 ) )
17 ssdomg ⊢ ( ( 𝐴 × ran 𝐹 ) ∈ V → ( 𝐹 ⊆ ( 𝐴 × ran 𝐹 ) → 𝐹 ≼ ( 𝐴 × ran 𝐹 ) ) )
18 11 16 17 sylc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → 𝐹 ≼ ( 𝐴 × ran 𝐹 ) )
19 xpdom1g ⊢ ( ( ran 𝐹 ∈ V ∧ 𝐴 ≼ ω ) → ( 𝐴 × ran 𝐹 ) ≼ ( ω × ran 𝐹 ) )
20 10 19 sylancom ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → ( 𝐴 × ran 𝐹 ) ≼ ( ω × ran 𝐹 ) )
21 omex ⊢ ω ∈ V
22 fnrndomg ⊢ ( 𝐴 ∈ V → ( 𝐹 Fn 𝐴 → ran 𝐹 ≼ 𝐴 ) )
23 2 12 22 sylc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → ran 𝐹 ≼ 𝐴 )
24 domtr ⊢ ( ( ran 𝐹 ≼ 𝐴 ∧ 𝐴 ≼ ω ) → ran 𝐹 ≼ ω )
25 23 24 sylancom ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → ran 𝐹 ≼ ω )
26 xpdom2g ⊢ ( ( ω ∈ V ∧ ran 𝐹 ≼ ω ) → ( ω × ran 𝐹 ) ≼ ( ω × ω ) )
27 21 25 26 sylancr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → ( ω × ran 𝐹 ) ≼ ( ω × ω ) )
28 domtr ⊢ ( ( ( 𝐴 × ran 𝐹 ) ≼ ( ω × ran 𝐹 ) ∧ ( ω × ran 𝐹 ) ≼ ( ω × ω ) ) → ( 𝐴 × ran 𝐹 ) ≼ ( ω × ω ) )
29 20 27 28 syl2anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → ( 𝐴 × ran 𝐹 ) ≼ ( ω × ω ) )
30 xpomen ⊢ ( ω × ω ) ≈ ω
31 domentr ⊢ ( ( ( 𝐴 × ran 𝐹 ) ≼ ( ω × ω ) ∧ ( ω × ω ) ≈ ω ) → ( 𝐴 × ran 𝐹 ) ≼ ω )
32 29 30 31 sylancl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → ( 𝐴 × ran 𝐹 ) ≼ ω )
33 domtr ⊢ ( ( 𝐹 ≼ ( 𝐴 × ran 𝐹 ) ∧ ( 𝐴 × ran 𝐹 ) ≼ ω ) → 𝐹 ≼ ω )
34 18 32 33 syl2anc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω ) → 𝐹 ≼ ω )