Metamath Proof Explorer

Theorem cnvct

Description: If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016)

Ref Expression
Assertion cnvct 
|- ( A ~<_ _om -> `' A ~<_ _om )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' A
2 ctex 
 |-  ( A ~<_ _om -> A e. _V )
3 cnvexg 
 |-  ( A e. _V -> `' A e. _V )
4 2 3 syl 
 |-  ( A ~<_ _om -> `' A e. _V )
5 cnven 
 |-  ( ( Rel `' A /\ `' A e. _V ) -> `' A ~~ `' `' A )
6 1 4 5 sylancr 
 |-  ( A ~<_ _om -> `' A ~~ `' `' A )
7 cnvcnvss 
 |-  `' `' A C_ A
8 ssdomg 
 |-  ( A e. _V -> ( `' `' A C_ A -> `' `' A ~<_ A ) )
9 2 7 8 mpisyl 
 |-  ( A ~<_ _om -> `' `' A ~<_ A )
10 endomtr 
 |-  ( ( `' A ~~ `' `' A /\ `' `' A ~<_ A ) -> `' A ~<_ A )
11 6 9 10 syl2anc 
 |-  ( A ~<_ _om -> `' A ~<_ A )
12 domtr 
 |-  ( ( `' A ~<_ A /\ A ~<_ _om ) -> `' A ~<_ _om )
13 11 12 mpancom 
 |-  ( A ~<_ _om -> `' A ~<_ _om )