f1ocnvd

Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	f1od.1	$⊢ F = (x \in A ⟼ C)$
	f1od.2	$⊢ (φ \land x \in A) \to C \in W$
	f1od.3	$⊢ (φ \land y \in B) \to D \in X$
	f1od.4	$⊢ φ \to ((x \in A \land y = C) \leftrightarrow (y \in B \land x = D))$
Assertion	f1ocnvd	$⊢ φ \to (F : A \underset{1-1 onto}{⟶} B \land F^{-1} = (y \in B ⟼ D))$

Step	Hyp	Ref	Expression
1		f1od.1	$⊢ F = (x \in A ⟼ C)$
2		f1od.2	$⊢ (φ \land x \in A) \to C \in W$
3		f1od.3	$⊢ (φ \land y \in B) \to D \in X$
4		f1od.4	$⊢ φ \to ((x \in A \land y = C) \leftrightarrow (y \in B \land x = D))$
5	2	ralrimiva	$⊢ φ \to \forall x \in A C \in W$
6	1	fnmpt	$⊢ \forall x \in A C \in W \to F Fn A$
7	5 6	syl	$⊢ φ \to F Fn A$
8	3	ralrimiva	$⊢ φ \to \forall y \in B D \in X$
9		eqid	$⊢ (y \in B ⟼ D) = (y \in B ⟼ D)$
10	9	fnmpt	$⊢ \forall y \in B D \in X \to (y \in B ⟼ D) Fn B$
11	8 10	syl	$⊢ φ \to (y \in B ⟼ D) Fn B$
12	4	opabbidv	$⊢ φ \to \{⟨y, x⟩ \| (x \in A \land y = C)\} = \{⟨y, x⟩ \| (y \in B \land x = D)\}$
13		df-mpt	$⊢ (x \in A ⟼ C) = \{⟨x, y⟩ \| (x \in A \land y = C)\}$
14	1 13	eqtri	$⊢ F = \{⟨x, y⟩ \| (x \in A \land y = C)\}$
15	14	cnveqi	$⊢ F^{-1} = {\{⟨x, y⟩ \| (x \in A \land y = C)\}}^{-1}$
16		cnvopab	$⊢ {\{⟨x, y⟩ \| (x \in A \land y = C)\}}^{-1} = \{⟨y, x⟩ \| (x \in A \land y = C)\}$
17	15 16	eqtri	$⊢ F^{-1} = \{⟨y, x⟩ \| (x \in A \land y = C)\}$
18		df-mpt	$⊢ (y \in B ⟼ D) = \{⟨y, x⟩ \| (y \in B \land x = D)\}$
19	12 17 18	3eqtr4g	$⊢ φ \to F^{-1} = (y \in B ⟼ D)$
20	19	fneq1d	$⊢ φ \to (F^{-1} Fn B \leftrightarrow (y \in B ⟼ D) Fn B)$
21	11 20	mpbird	$⊢ φ \to F^{-1} Fn B$
22		dff1o4	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F Fn A \land F^{-1} Fn B)$
23	7 21 22	sylanbrc	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$
24	23 19	jca	$⊢ φ \to (F : A \underset{1-1 onto}{⟶} B \land F^{-1} = (y \in B ⟼ D))$

Metamath Proof Explorer