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 )