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 ~<_ _om ) -> F ~<_ _om )

Proof

Step Hyp Ref Expression
1 ctex
 |-  ( A ~<_ _om -> A e. _V )
2 1 adantl
 |-  ( ( F Fn A /\ A ~<_ _om ) -> A e. _V )
3 fndm
 |-  ( F Fn A -> dom F = A )
4 3 eleq1d
 |-  ( F Fn A -> ( dom F e. _V <-> A e. _V ) )
5 4 adantr
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( dom F e. _V <-> A e. _V ) )
6 2 5 mpbird
 |-  ( ( F Fn A /\ A ~<_ _om ) -> dom F e. _V )
7 fnfun
 |-  ( F Fn A -> Fun F )
8 7 adantr
 |-  ( ( F Fn A /\ A ~<_ _om ) -> Fun F )
9 funrnex
 |-  ( dom F e. _V -> ( Fun F -> ran F e. _V ) )
10 6 8 9 sylc
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ran F e. _V )
11 2 10 xpexd
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( A X. ran F ) e. _V )
12 simpl
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F Fn A )
13 dffn3
 |-  ( F Fn A <-> F : A --> ran F )
14 12 13 sylib
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F : A --> ran F )
15 fssxp
 |-  ( F : A --> ran F -> F C_ ( A X. ran F ) )
16 14 15 syl
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F C_ ( A X. ran F ) )
17 ssdomg
 |-  ( ( A X. ran F ) e. _V -> ( F C_ ( A X. ran F ) -> F ~<_ ( A X. ran F ) ) )
18 11 16 17 sylc
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F ~<_ ( A X. ran F ) )
19 xpdom1g
 |-  ( ( ran F e. _V /\ A ~<_ _om ) -> ( A X. ran F ) ~<_ ( _om X. ran F ) )
20 10 19 sylancom
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( A X. ran F ) ~<_ ( _om X. ran F ) )
21 omex
 |-  _om e. _V
22 fnrndomg
 |-  ( A e. _V -> ( F Fn A -> ran F ~<_ A ) )
23 2 12 22 sylc
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ran F ~<_ A )
24 domtr
 |-  ( ( ran F ~<_ A /\ A ~<_ _om ) -> ran F ~<_ _om )
25 23 24 sylancom
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ran F ~<_ _om )
26 xpdom2g
 |-  ( ( _om e. _V /\ ran F ~<_ _om ) -> ( _om X. ran F ) ~<_ ( _om X. _om ) )
27 21 25 26 sylancr
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( _om X. ran F ) ~<_ ( _om X. _om ) )
28 domtr
 |-  ( ( ( A X. ran F ) ~<_ ( _om X. ran F ) /\ ( _om X. ran F ) ~<_ ( _om X. _om ) ) -> ( A X. ran F ) ~<_ ( _om X. _om ) )
29 20 27 28 syl2anc
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( A X. ran F ) ~<_ ( _om X. _om ) )
30 xpomen
 |-  ( _om X. _om ) ~~ _om
31 domentr
 |-  ( ( ( A X. ran F ) ~<_ ( _om X. _om ) /\ ( _om X. _om ) ~~ _om ) -> ( A X. ran F ) ~<_ _om )
32 29 30 31 sylancl
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( A X. ran F ) ~<_ _om )
33 domtr
 |-  ( ( F ~<_ ( A X. ran F ) /\ ( A X. ran F ) ~<_ _om ) -> F ~<_ _om )
34 18 32 33 syl2anc
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F ~<_ _om )