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 ( 𝐴 ≼ ω → 𝐴 ≼ ω )

Proof

Step Hyp Ref Expression
1 relcnv Rel 𝐴
2 ctex ( 𝐴 ≼ ω → 𝐴 ∈ V )
3 cnvexg ( 𝐴 ∈ V → 𝐴 ∈ V )
4 2 3 syl ( 𝐴 ≼ ω → 𝐴 ∈ V )
5 cnven ( ( Rel 𝐴 𝐴 ∈ V ) → 𝐴 𝐴 )
6 1 4 5 sylancr ( 𝐴 ≼ ω → 𝐴 𝐴 )
7 cnvcnvss 𝐴𝐴
8 ssdomg ( 𝐴 ∈ V → ( 𝐴𝐴 𝐴𝐴 ) )
9 2 7 8 mpisyl ( 𝐴 ≼ ω → 𝐴𝐴 )
10 endomtr ( ( 𝐴 𝐴 𝐴𝐴 ) → 𝐴𝐴 )
11 6 9 10 syl2anc ( 𝐴 ≼ ω → 𝐴𝐴 )
12 domtr ( ( 𝐴𝐴𝐴 ≼ ω ) → 𝐴 ≼ ω )
13 11 12 mpancom ( 𝐴 ≼ ω → 𝐴 ≼ ω )