Metamath Proof Explorer

Theorem fnct

Description: If the domain of a function is countable, the function is countable. The proof uses fnrndomnum rather than fnrndomg , and so does not require ax-ac . (Contributed by Thierry Arnoux, 29-Dec-2016) (Revised by Vincent Gonzalez, 24-Aug-2026)

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 dffn3 
 |-  ( F Fn A <-> F : A --> ran F )
13 12 birani 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F : A --> ran F )
14 fssxp 
 |-  ( F : A --> ran F -> F C_ ( A X. ran F ) )
15 13 14 syl 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F C_ ( A X. ran F ) )
16 ssdomg 
 |-  ( ( A X. ran F ) e. _V -> ( F C_ ( A X. ran F ) -> F ~<_ ( A X. ran F ) ) )
17 11 15 16 sylc 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F ~<_ ( A X. ran F ) )
18 xpdom1g 
 |-  ( ( ran F e. _V /\ A ~<_ _om ) -> ( A X. ran F ) ~<_ ( _om X. ran F ) )
19 10 18 sylancom 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( A X. ran F ) ~<_ ( _om X. ran F ) )
20 omex 
 |-  _om e. _V
21 omelon 
 |-  _om e. On
22 21 a1i 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> _om e. On )
23 simpr 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> A ~<_ _om )
24 ondomen 
 |-  ( ( _om e. On /\ A ~<_ _om ) -> A e. dom card )
25 22 23 24 syl2anc 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> A e. dom card )
26 simpl 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F Fn A )
27 fnrndomnum 
 |-  ( A e. dom card -> ( F Fn A -> ran F ~<_ A ) )
28 25 26 27 sylc 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ran F ~<_ A )
29 domtr 
 |-  ( ( ran F ~<_ A /\ A ~<_ _om ) -> ran F ~<_ _om )
30 28 29 sylancom 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ran F ~<_ _om )
31 xpdom2g 
 |-  ( ( _om e. _V /\ ran F ~<_ _om ) -> ( _om X. ran F ) ~<_ ( _om X. _om ) )
32 20 30 31 sylancr 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( _om X. ran F ) ~<_ ( _om X. _om ) )
33 domtr 
 |-  ( ( ( A X. ran F ) ~<_ ( _om X. ran F ) /\ ( _om X. ran F ) ~<_ ( _om X. _om ) ) -> ( A X. ran F ) ~<_ ( _om X. _om ) )
34 19 32 33 syl2anc 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( A X. ran F ) ~<_ ( _om X. _om ) )
35 xpomen 
 |-  ( _om X. _om ) ~~ _om
36 domentr 
 |-  ( ( ( A X. ran F ) ~<_ ( _om X. _om ) /\ ( _om X. _om ) ~~ _om ) -> ( A X. ran F ) ~<_ _om )
37 34 35 36 sylancl 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> ( A X. ran F ) ~<_ _om )
38 domtr 
 |-  ( ( F ~<_ ( A X. ran F ) /\ ( A X. ran F ) ~<_ _om ) -> F ~<_ _om )
39 17 37 38 syl2anc 
 |-  ( ( F Fn A /\ A ~<_ _om ) -> F ~<_ _om )