f1o3d

Description: Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		f1o3d.1	$⊢ φ \to F = (x \in A ⟼ C)$
2		f1o3d.2	$⊢ (φ \land x \in A) \to C \in B$
3		f1o3d.3	$⊢ (φ \land y \in B) \to D \in A$
4		f1o3d.4	$⊢ (φ \land (x \in A \land y \in B)) \to (x = D \leftrightarrow y = C)$
5	2	ralrimiva	$⊢ φ \to \forall x \in A C \in B$
6		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
7	6	fnmpt	$⊢ \forall x \in A C \in B \to (x \in A ⟼ C) Fn A$
8	5 7	syl	$⊢ φ \to (x \in A ⟼ C) Fn A$
9	1	fneq1d	$⊢ φ \to (F Fn A \leftrightarrow (x \in A ⟼ C) Fn A)$
10	8 9	mpbird	$⊢ φ \to F Fn A$
11	3	ralrimiva	$⊢ φ \to \forall y \in B D \in A$
12		eqid	$⊢ (y \in B ⟼ D) = (y \in B ⟼ D)$
13	12	fnmpt	$⊢ \forall y \in B D \in A \to (y \in B ⟼ D) Fn B$
14	11 13	syl	$⊢ φ \to (y \in B ⟼ D) Fn B$
15		eleq1a	$⊢ C \in B \to (y = C \to y \in B)$
16	2 15	syl	$⊢ (φ \land x \in A) \to (y = C \to y \in B)$
17	16	impr	$⊢ (φ \land (x \in A \land y = C)) \to y \in B$
18	4	biimpar	$⊢ ((φ \land (x \in A \land y \in B)) \land y = C) \to x = D$
19	18	exp42	$⊢ φ \to (x \in A \to (y \in B \to (y = C \to x = D)))$
20	19	com34	$⊢ φ \to (x \in A \to (y = C \to (y \in B \to x = D)))$
21	20	imp32	$⊢ (φ \land (x \in A \land y = C)) \to (y \in B \to x = D)$
22	17 21	jcai	$⊢ (φ \land (x \in A \land y = C)) \to (y \in B \land x = D)$
23		eleq1a	$⊢ D \in A \to (x = D \to x \in A)$
24	3 23	syl	$⊢ (φ \land y \in B) \to (x = D \to x \in A)$
25	24	impr	$⊢ (φ \land (y \in B \land x = D)) \to x \in A$
26	4	biimpa	$⊢ ((φ \land (x \in A \land y \in B)) \land x = D) \to y = C$
27	26	exp42	$⊢ φ \to (x \in A \to (y \in B \to (x = D \to y = C)))$
28	27	com23	$⊢ φ \to (y \in B \to (x \in A \to (x = D \to y = C)))$
29	28	com34	$⊢ φ \to (y \in B \to (x = D \to (x \in A \to y = C)))$
30	29	imp32	$⊢ (φ \land (y \in B \land x = D)) \to (x \in A \to y = C)$
31	25 30	jcai	$⊢ (φ \land (y \in B \land x = D)) \to (x \in A \land y = C)$
32	22 31	impbida	$⊢ φ \to ((x \in A \land y = C) \leftrightarrow (y \in B \land x = D))$
33	32	opabbidv	$⊢ φ \to \{⟨y, x⟩ \| (x \in A \land y = C)\} = \{⟨y, x⟩ \| (y \in B \land x = D)\}$
34		df-mpt	$⊢ (x \in A ⟼ C) = \{⟨x, y⟩ \| (x \in A \land y = C)\}$
35	1 34	eqtrdi	$⊢ φ \to F = \{⟨x, y⟩ \| (x \in A \land y = C)\}$
36	35	cnveqd	$⊢ φ \to F^{-1} = {\{⟨x, y⟩ \| (x \in A \land y = C)\}}^{-1}$
37		cnvopab	$⊢ {\{⟨x, y⟩ \| (x \in A \land y = C)\}}^{-1} = \{⟨y, x⟩ \| (x \in A \land y = C)\}$
38	36 37	eqtrdi	$⊢ φ \to F^{-1} = \{⟨y, x⟩ \| (x \in A \land y = C)\}$
39		df-mpt	$⊢ (y \in B ⟼ D) = \{⟨y, x⟩ \| (y \in B \land x = D)\}$
40	39	a1i	$⊢ φ \to (y \in B ⟼ D) = \{⟨y, x⟩ \| (y \in B \land x = D)\}$
41	33 38 40	3eqtr4d	$⊢ φ \to F^{-1} = (y \in B ⟼ D)$
42	41	fneq1d	$⊢ φ \to (F^{-1} Fn B \leftrightarrow (y \in B ⟼ D) Fn B)$
43	14 42	mpbird	$⊢ φ \to F^{-1} Fn B$
44		dff1o4	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F Fn A \land F^{-1} Fn B)$
45	10 43 44	sylanbrc	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$
46	45 41	jca	$⊢ φ \to (F : A \underset{1-1 onto}{⟶} B \land F^{-1} = (y \in B ⟼ D))$

Metamath Proof Explorer

Theorem f1o3d

Proof