f1ompt

Description: Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015) (Revised by Mario Carneiro, 4-Dec-2016)

		Ref	Expression
	Hypothesis	fmpt.1	$⊢ F = (x \in A ⟼ C)$
	Assertion	f1ompt	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (\forall x \in A C \in B \land \forall y \in B \exists! x \in A y = C)$

Proof

Step	Hyp	Ref	Expression
1		fmpt.1	$⊢ F = (x \in A ⟼ C)$
2		ffn	$⊢ F : A ⟶ B \to F Fn A$
3		dff1o4	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F Fn A \land F^{-1} Fn B)$
4	3	baib	$⊢ F Fn A \to (F : A \underset{1-1 onto}{⟶} B \leftrightarrow F^{-1} Fn B)$
5	2 4	syl	$⊢ F : A ⟶ B \to (F : A \underset{1-1 onto}{⟶} B \leftrightarrow F^{-1} Fn B)$
6		fnres	$⊢ ({F^{-1} ↾}_{B}) Fn B \leftrightarrow \forall y \in B \exists! z y F^{-1} z$
7		nfcv	$⊢ \underline{Ⅎ} x z$
8		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C)$
9	1 8	nfcxfr	$⊢ \underline{Ⅎ} x F$
10		nfcv	$⊢ \underline{Ⅎ} x y$
11	7 9 10	nfbr	$⊢ Ⅎ x z F y$
12		nfv	$⊢ Ⅎ z (x \in A \land y = C)$
13		breq1	$⊢ z = x \to (z F y \leftrightarrow x F y)$
14		df-mpt	$⊢ (x \in A ⟼ C) = \{⟨x, y⟩ \| (x \in A \land y = C)\}$
15	1 14	eqtri	$⊢ F = \{⟨x, y⟩ \| (x \in A \land y = C)\}$
16	15	breqi	$⊢ x F y \leftrightarrow x \{⟨x, y⟩ \| (x \in A \land y = C)\} y$
17		df-br	$⊢ x \{⟨x, y⟩ \| (x \in A \land y = C)\} y \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in A \land y = C)\}$
18		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in A \land y = C)\} \leftrightarrow (x \in A \land y = C)$
19	17 18	bitri	$⊢ x \{⟨x, y⟩ \| (x \in A \land y = C)\} y \leftrightarrow (x \in A \land y = C)$
20	16 19	bitri	$⊢ x F y \leftrightarrow (x \in A \land y = C)$
21	13 20	bitrdi	$⊢ z = x \to (z F y \leftrightarrow (x \in A \land y = C))$
22	11 12 21	cbveuw	$⊢ \exists! z z F y \leftrightarrow \exists! x (x \in A \land y = C)$
23		vex	$⊢ y \in V$
24		vex	$⊢ z \in V$
25	23 24	brcnv	$⊢ y F^{-1} z \leftrightarrow z F y$
26	25	eubii	$⊢ \exists! z y F^{-1} z \leftrightarrow \exists! z z F y$
27		df-reu	$⊢ \exists! x \in A y = C \leftrightarrow \exists! x (x \in A \land y = C)$
28	22 26 27	3bitr4i	$⊢ \exists! z y F^{-1} z \leftrightarrow \exists! x \in A y = C$
29	28	ralbii	$⊢ \forall y \in B \exists! z y F^{-1} z \leftrightarrow \forall y \in B \exists! x \in A y = C$
30	6 29	bitri	$⊢ ({F^{-1} ↾}_{B}) Fn B \leftrightarrow \forall y \in B \exists! x \in A y = C$
31		relcnv	$⊢ Rel F^{-1}$
32		df-rn	$⊢ ran F = dom F^{-1}$
33		frn	$⊢ F : A ⟶ B \to ran F \subseteq B$
34	32 33	eqsstrrid	$⊢ F : A ⟶ B \to dom F^{-1} \subseteq B$
35		relssres	$⊢ (Rel F^{-1} \land dom F^{-1} \subseteq B) \to {F^{-1} ↾}_{B} = F^{-1}$
36	31 34 35	sylancr	$⊢ F : A ⟶ B \to {F^{-1} ↾}_{B} = F^{-1}$
37	36	fneq1d	$⊢ F : A ⟶ B \to (({F^{-1} ↾}_{B}) Fn B \leftrightarrow F^{-1} Fn B)$
38	30 37	bitr3id	$⊢ F : A ⟶ B \to (\forall y \in B \exists! x \in A y = C \leftrightarrow F^{-1} Fn B)$
39	5 38	bitr4d	$⊢ F : A ⟶ B \to (F : A \underset{1-1 onto}{⟶} B \leftrightarrow \forall y \in B \exists! x \in A y = C)$
40	39	pm5.32i	$⊢ (F : A ⟶ B \land F : A \underset{1-1 onto}{⟶} B) \leftrightarrow (F : A ⟶ B \land \forall y \in B \exists! x \in A y = C)$
41		f1of	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A ⟶ B$
42	41	pm4.71ri	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F : A ⟶ B \land F : A \underset{1-1 onto}{⟶} B)$
43	1	fmpt	$⊢ \forall x \in A C \in B \leftrightarrow F : A ⟶ B$
44	43	anbi1i	$⊢ (\forall x \in A C \in B \land \forall y \in B \exists! x \in A y = C) \leftrightarrow (F : A ⟶ B \land \forall y \in B \exists! x \in A y = C)$
45	40 42 44	3bitr4i	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (\forall x \in A C \in B \land \forall y \in B \exists! x \in A y = C)$

Metamath Proof Explorer

Theorem f1ompt

Proof