Theorem cnven

Description: A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Assertion	cnven	⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ≈ ◡ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
2		cnvexg	⊢ ( 𝐴 ∈ 𝑉 → ◡ 𝐴 ∈ V )
3	2	adantl	⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ◡ 𝐴 ∈ V )
4		cnvf1o	⊢ ( Rel 𝐴 → ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : 𝐴 –1-1-onto→ ◡ 𝐴 )
5	4	adantr	⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : 𝐴 –1-1-onto→ ◡ 𝐴 )
6		f1oen2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ◡ 𝐴 ∈ V ∧ ( 𝑥 ∈ 𝐴 ↦ ∪ ◡ { 𝑥 } ) : 𝐴 –1-1-onto→ ◡ 𝐴 ) → 𝐴 ≈ ◡ 𝐴 )
7	1 3 5 6	syl3anc	⊢ ( ( Rel 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ≈ ◡ 𝐴 )