Metamath Proof Explorer


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 𝐴𝐴𝑉 ) → 𝐴 𝐴 )