cnven

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

		Ref	Expression
	Assertion	cnven	$⊢ (Rel A \land A \in V) \to A \approx A^{-1}$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (Rel A \land A \in V) \to A \in V$
2		cnvexg	$⊢ A \in V \to A^{-1} \in V$
3	2	adantl	$⊢ (Rel A \land A \in V) \to A^{-1} \in V$
4		cnvf1o	$⊢ Rel A \to (x \in A ⟼ ⋃ {\{x\}}^{-1}) : A \underset{1-1 onto}{⟶} A^{-1}$
5	4	adantr	$⊢ (Rel A \land A \in V) \to (x \in A ⟼ ⋃ {\{x\}}^{-1}) : A \underset{1-1 onto}{⟶} A^{-1}$
6		f1oen2g	$⊢ (A \in V \land A^{-1} \in V \land (x \in A ⟼ ⋃ {\{x\}}^{-1}) : A \underset{1-1 onto}{⟶} A^{-1}) \to A \approx A^{-1}$
7	1 3 5 6	syl3anc	$⊢ (Rel A \land A \in V) \to A \approx A^{-1}$

Metamath Proof Explorer