This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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