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 ⊢ A ≼ ω → A -1 ≼ ω

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ⁡ A -1
2 ctex ⊢ A ≼ ω → A ∈ V
3 cnvexg ⊢ A ∈ V → A -1 ∈ V
4 2 3 syl ⊢ A ≼ ω → A -1 ∈ V
5 cnven ⊢ Rel ⁡ A -1 ∧ A -1 ∈ V → A -1 ≈ A -1 -1
6 1 4 5 sylancr ⊢ A ≼ ω → A -1 ≈ A -1 -1
7 cnvcnvss ⊢ A -1 -1 ⊆ A
8 ssdomg ⊢ A ∈ V → A -1 -1 ⊆ A → A -1 -1 ≼ A
9 2 7 8 mpisyl ⊢ A ≼ ω → A -1 -1 ≼ A
10 endomtr ⊢ A -1 ≈ A -1 -1 ∧ A -1 -1 ≼ A → A -1 ≼ A
11 6 9 10 syl2anc ⊢ A ≼ ω → A -1 ≼ A
12 domtr ⊢ A -1 ≼ A ∧ A ≼ ω → A -1 ≼ ω
13 11 12 mpancom ⊢ A ≼ ω → A -1 ≼ ω