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