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 )