Metamath Proof Explorer

Theorem dmct

Description: The domain of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016)

Ref Expression
Assertion dmct 
|- ( A ~<_ _om -> dom A ~<_ _om )

Proof

Step Hyp Ref Expression
1 dmresv 
 |-  dom ( A |` _V ) = dom A
2 resss 
 |-  ( A |` _V ) C_ A
3 ctex 
 |-  ( A ~<_ _om -> A e. _V )
4 ssexg 
 |-  ( ( ( A |` _V ) C_ A /\ A e. _V ) -> ( A |` _V ) e. _V )
5 2 3 4 sylancr 
 |-  ( A ~<_ _om -> ( A |` _V ) e. _V )
6 fvex 
 |-  ( 1st ` x ) e. _V
7 eqid 
 |-  ( x e. ( A |` _V ) |-> ( 1st ` x ) ) = ( x e. ( A |` _V ) |-> ( 1st ` x ) )
8 6 7 fnmpti 
 |-  ( x e. ( A |` _V ) |-> ( 1st ` x ) ) Fn ( A |` _V )
9 dffn4 
 |-  ( ( x e. ( A |` _V ) |-> ( 1st ` x ) ) Fn ( A |` _V ) <-> ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) )
10 8 9 mpbi 
 |-  ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> ran ( x e. ( A |` _V ) |-> ( 1st ` x ) )
11 relres 
 |-  Rel ( A |` _V )
12 reldm 
 |-  ( Rel ( A |` _V ) -> dom ( A |` _V ) = ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) )
13 foeq3 
 |-  ( dom ( A |` _V ) = ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) -> ( ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> dom ( A |` _V ) <-> ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) ) )
14 11 12 13 mp2b 
 |-  ( ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> dom ( A |` _V ) <-> ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> ran ( x e. ( A |` _V ) |-> ( 1st ` x ) ) )
15 10 14 mpbir 
 |-  ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> dom ( A |` _V )
16 fodomg 
 |-  ( ( A |` _V ) e. _V -> ( ( x e. ( A |` _V ) |-> ( 1st ` x ) ) : ( A |` _V ) -onto-> dom ( A |` _V ) -> dom ( A |` _V ) ~<_ ( A |` _V ) ) )
17 5 15 16 mpisyl 
 |-  ( A ~<_ _om -> dom ( A |` _V ) ~<_ ( A |` _V ) )
18 ssdomg 
 |-  ( A e. _V -> ( ( A |` _V ) C_ A -> ( A |` _V ) ~<_ A ) )
19 3 2 18 mpisyl 
 |-  ( A ~<_ _om -> ( A |` _V ) ~<_ A )
20 domtr 
 |-  ( ( ( A |` _V ) ~<_ A /\ A ~<_ _om ) -> ( A |` _V ) ~<_ _om )
21 19 20 mpancom 
 |-  ( A ~<_ _om -> ( A |` _V ) ~<_ _om )
22 domtr 
 |-  ( ( dom ( A |` _V ) ~<_ ( A |` _V ) /\ ( A |` _V ) ~<_ _om ) -> dom ( A |` _V ) ~<_ _om )
23 17 21 22 syl2anc 
 |-  ( A ~<_ _om -> dom ( A |` _V ) ~<_ _om )
24 1 23 eqbrtrrid 
 |-  ( A ~<_ _om -> dom A ~<_ _om )