xpcomf1o

Description: The canonical bijection from ( A X. B ) to ( B X. A ) . (Contributed by Mario Carneiro, 23-Apr-2014)

		Ref	Expression
	Hypothesis	xpcomf1o.1	$⊢ F = (x \in (A \times B) ⟼ ⋃ {\{x\}}^{-1})$
	Assertion	xpcomf1o	$⊢ F : A \times B \underset{1-1 onto}{⟶} B \times A$

Step	Hyp	Ref	Expression
1		xpcomf1o.1	$⊢ F = (x \in (A \times B) ⟼ ⋃ {\{x\}}^{-1})$
2		relxp	$⊢ Rel (A \times B)$
3		cnvf1o	$⊢ Rel (A \times B) \to (x \in (A \times B) ⟼ ⋃ {\{x\}}^{-1}) : A \times B \underset{1-1 onto}{⟶} {(A \times B)}^{-1}$
4	2 3	ax-mp	$⊢ (x \in (A \times B) ⟼ ⋃ {\{x\}}^{-1}) : A \times B \underset{1-1 onto}{⟶} {(A \times B)}^{-1}$
5		f1oeq1	$⊢ F = (x \in (A \times B) ⟼ ⋃ {\{x\}}^{-1}) \to (F : A \times B \underset{1-1 onto}{⟶} {(A \times B)}^{-1} \leftrightarrow (x \in (A \times B) ⟼ ⋃ {\{x\}}^{-1}) : A \times B \underset{1-1 onto}{⟶} {(A \times B)}^{-1})$
6	1 5	ax-mp	$⊢ F : A \times B \underset{1-1 onto}{⟶} {(A \times B)}^{-1} \leftrightarrow (x \in (A \times B) ⟼ ⋃ {\{x\}}^{-1}) : A \times B \underset{1-1 onto}{⟶} {(A \times B)}^{-1}$
7	4 6	mpbir	$⊢ F : A \times B \underset{1-1 onto}{⟶} {(A \times B)}^{-1}$
8		cnvxp	$⊢ {(A \times B)}^{-1} = B \times A$
9		f1oeq3	$⊢ {(A \times B)}^{-1} = B \times A \to (F : A \times B \underset{1-1 onto}{⟶} {(A \times B)}^{-1} \leftrightarrow F : A \times B \underset{1-1 onto}{⟶} B \times A)$
10	8 9	ax-mp	$⊢ F : A \times B \underset{1-1 onto}{⟶} {(A \times B)}^{-1} \leftrightarrow F : A \times B \underset{1-1 onto}{⟶} B \times A$
11	7 10	mpbi	$⊢ F : A \times B \underset{1-1 onto}{⟶} B \times A$

Metamath Proof Explorer