f1o2ndf1

Description: The 2nd (second component of an ordered pair) function restricted to a one-to-one function F is a one-to-one function from F onto the range of F . (Contributed by Alexander van der Vekens, 4-Feb-2018)

		Ref	Expression
	Assertion	f1o2ndf1	$⊢ F : A \underset{1-1}{⟶} B \to ({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
2		fo2ndf	$⊢ F : A ⟶ B \to ({2^{nd} ↾}_{F}) : F \underset{onto}{⟶} ran F$
3	1 2	syl	$⊢ F : A \underset{1-1}{⟶} B \to ({2^{nd} ↾}_{F}) : F \underset{onto}{⟶} ran F$
4		f2ndf	$⊢ F : A ⟶ B \to ({2^{nd} ↾}_{F}) : F ⟶ B$
5	1 4	syl	$⊢ F : A \underset{1-1}{⟶} B \to ({2^{nd} ↾}_{F}) : F ⟶ B$
6		fssxp	$⊢ F : A ⟶ B \to F \subseteq A \times B$
7	1 6	syl	$⊢ F : A \underset{1-1}{⟶} B \to F \subseteq A \times B$
8		ssel2	$⊢ (F \subseteq A \times B \land x \in F) \to x \in (A \times B)$
9		elxp2	$⊢ x \in (A \times B) \leftrightarrow \exists a \in A \exists v \in B x = ⟨a, v⟩$
10	8 9	sylib	$⊢ (F \subseteq A \times B \land x \in F) \to \exists a \in A \exists v \in B x = ⟨a, v⟩$
11		ssel2	$⊢ (F \subseteq A \times B \land y \in F) \to y \in (A \times B)$
12		elxp2	$⊢ y \in (A \times B) \leftrightarrow \exists b \in A \exists w \in B y = ⟨b, w⟩$
13	11 12	sylib	$⊢ (F \subseteq A \times B \land y \in F) \to \exists b \in A \exists w \in B y = ⟨b, w⟩$
14	10 13	anim12dan	$⊢ (F \subseteq A \times B \land (x \in F \land y \in F)) \to (\exists a \in A \exists v \in B x = ⟨a, v⟩ \land \exists b \in A \exists w \in B y = ⟨b, w⟩)$
15		fvres	$⊢ ⟨a, v⟩ \in F \to ({2^{nd} ↾}_{F}) (⟨a, v⟩) = 2^{nd} (⟨a, v⟩)$
16	15	ad2antrr	$⊢ ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to ({2^{nd} ↾}_{F}) (⟨a, v⟩) = 2^{nd} (⟨a, v⟩)$
17		fvres	$⊢ ⟨b, w⟩ \in F \to ({2^{nd} ↾}_{F}) (⟨b, w⟩) = 2^{nd} (⟨b, w⟩)$
18	17	ad2antlr	$⊢ ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to ({2^{nd} ↾}_{F}) (⟨b, w⟩) = 2^{nd} (⟨b, w⟩)$
19	16 18	eqeq12d	$⊢ ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to (({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩) \leftrightarrow 2^{nd} (⟨a, v⟩) = 2^{nd} (⟨b, w⟩))$
20		vex	$⊢ a \in V$
21		vex	$⊢ v \in V$
22	20 21	op2nd	$⊢ 2^{nd} (⟨a, v⟩) = v$
23		vex	$⊢ b \in V$
24		vex	$⊢ w \in V$
25	23 24	op2nd	$⊢ 2^{nd} (⟨b, w⟩) = w$
26	22 25	eqeq12i	$⊢ 2^{nd} (⟨a, v⟩) = 2^{nd} (⟨b, w⟩) \leftrightarrow v = w$
27		f1fun	$⊢ F : A \underset{1-1}{⟶} B \to Fun F$
28		funopfv	$⊢ Fun F \to (⟨a, v⟩ \in F \to F (a) = v)$
29		funopfv	$⊢ Fun F \to (⟨b, w⟩ \in F \to F (b) = w)$
30	28 29	anim12d	$⊢ Fun F \to ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \to (F (a) = v \land F (b) = w))$
31	27 30	syl	$⊢ F : A \underset{1-1}{⟶} B \to ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \to (F (a) = v \land F (b) = w))$
32		eqcom	$⊢ F (a) = v \leftrightarrow v = F (a)$
33	32	biimpi	$⊢ F (a) = v \to v = F (a)$
34		eqcom	$⊢ F (b) = w \leftrightarrow w = F (b)$
35	34	biimpi	$⊢ F (b) = w \to w = F (b)$
36	33 35	eqeqan12d	$⊢ (F (a) = v \land F (b) = w) \to (v = w \leftrightarrow F (a) = F (b))$
37		simpl	$⊢ (a \in A \land v \in B) \to a \in A$
38		simpl	$⊢ (b \in A \land w \in B) \to b \in A$
39	37 38	anim12i	$⊢ ((a \in A \land v \in B) \land (b \in A \land w \in B)) \to (a \in A \land b \in A)$
40		f1veqaeq	$⊢ (F : A \underset{1-1}{⟶} B \land (a \in A \land b \in A)) \to (F (a) = F (b) \to a = b)$
41	39 40	sylan2	$⊢ (F : A \underset{1-1}{⟶} B \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to (F (a) = F (b) \to a = b)$
42		opeq12	$⊢ (a = b \land v = w) \to ⟨a, v⟩ = ⟨b, w⟩$
43	42	ex	$⊢ a = b \to (v = w \to ⟨a, v⟩ = ⟨b, w⟩)$
44	41 43	syl6	$⊢ (F : A \underset{1-1}{⟶} B \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to (F (a) = F (b) \to (v = w \to ⟨a, v⟩ = ⟨b, w⟩))$
45	44	com23	$⊢ (F : A \underset{1-1}{⟶} B \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to (v = w \to (F (a) = F (b) \to ⟨a, v⟩ = ⟨b, w⟩))$
46	45	ex	$⊢ F : A \underset{1-1}{⟶} B \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to (v = w \to (F (a) = F (b) \to ⟨a, v⟩ = ⟨b, w⟩)))$
47	46	com14	$⊢ F (a) = F (b) \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to (v = w \to (F : A \underset{1-1}{⟶} B \to ⟨a, v⟩ = ⟨b, w⟩)))$
48	36 47	syl6bi	$⊢ (F (a) = v \land F (b) = w) \to (v = w \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to (v = w \to (F : A \underset{1-1}{⟶} B \to ⟨a, v⟩ = ⟨b, w⟩))))$
49	48	com14	$⊢ v = w \to (v = w \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to ((F (a) = v \land F (b) = w) \to (F : A \underset{1-1}{⟶} B \to ⟨a, v⟩ = ⟨b, w⟩))))$
50	49	pm2.43i	$⊢ v = w \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to ((F (a) = v \land F (b) = w) \to (F : A \underset{1-1}{⟶} B \to ⟨a, v⟩ = ⟨b, w⟩)))$
51	50	com14	$⊢ F : A \underset{1-1}{⟶} B \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to ((F (a) = v \land F (b) = w) \to (v = w \to ⟨a, v⟩ = ⟨b, w⟩)))$
52	51	com23	$⊢ F : A \underset{1-1}{⟶} B \to ((F (a) = v \land F (b) = w) \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to (v = w \to ⟨a, v⟩ = ⟨b, w⟩)))$
53	31 52	syld	$⊢ F : A \underset{1-1}{⟶} B \to ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to (v = w \to ⟨a, v⟩ = ⟨b, w⟩)))$
54	53	com13	$⊢ ((a \in A \land v \in B) \land (b \in A \land w \in B)) \to ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \to (F : A \underset{1-1}{⟶} B \to (v = w \to ⟨a, v⟩ = ⟨b, w⟩)))$
55	54	impcom	$⊢ ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to (F : A \underset{1-1}{⟶} B \to (v = w \to ⟨a, v⟩ = ⟨b, w⟩))$
56	55	com23	$⊢ ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to (v = w \to (F : A \underset{1-1}{⟶} B \to ⟨a, v⟩ = ⟨b, w⟩))$
57	26 56	syl5bi	$⊢ ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to (2^{nd} (⟨a, v⟩) = 2^{nd} (⟨b, w⟩) \to (F : A \underset{1-1}{⟶} B \to ⟨a, v⟩ = ⟨b, w⟩))$
58	19 57	sylbid	$⊢ ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to (({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩) \to (F : A \underset{1-1}{⟶} B \to ⟨a, v⟩ = ⟨b, w⟩))$
59	58	com23	$⊢ ((⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \land ((a \in A \land v \in B) \land (b \in A \land w \in B))) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩) \to ⟨a, v⟩ = ⟨b, w⟩))$
60	59	ex	$⊢ (⟨a, v⟩ \in F \land ⟨b, w⟩ \in F) \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩) \to ⟨a, v⟩ = ⟨b, w⟩)))$
61	60	adantl	$⊢ (F \subseteq A \times B \land (⟨a, v⟩ \in F \land ⟨b, w⟩ \in F)) \to (((a \in A \land v \in B) \land (b \in A \land w \in B)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩) \to ⟨a, v⟩ = ⟨b, w⟩)))$
62	61	com12	$⊢ ((a \in A \land v \in B) \land (b \in A \land w \in B)) \to ((F \subseteq A \times B \land (⟨a, v⟩ \in F \land ⟨b, w⟩ \in F)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩) \to ⟨a, v⟩ = ⟨b, w⟩)))$
63	62	ad4ant13	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to ((F \subseteq A \times B \land (⟨a, v⟩ \in F \land ⟨b, w⟩ \in F)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩) \to ⟨a, v⟩ = ⟨b, w⟩)))$
64		eleq1	$⊢ x = ⟨a, v⟩ \to (x \in F \leftrightarrow ⟨a, v⟩ \in F)$
65	64	ad2antlr	$⊢ (((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \to (x \in F \leftrightarrow ⟨a, v⟩ \in F)$
66		eleq1	$⊢ y = ⟨b, w⟩ \to (y \in F \leftrightarrow ⟨b, w⟩ \in F)$
67	65 66	bi2anan9	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to ((x \in F \land y \in F) \leftrightarrow (⟨a, v⟩ \in F \land ⟨b, w⟩ \in F))$
68	67	anbi2d	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to ((F \subseteq A \times B \land (x \in F \land y \in F)) \leftrightarrow (F \subseteq A \times B \land (⟨a, v⟩ \in F \land ⟨b, w⟩ \in F)))$
69		fveq2	$⊢ x = ⟨a, v⟩ \to ({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (⟨a, v⟩)$
70	69	ad2antlr	$⊢ (((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \to ({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (⟨a, v⟩)$
71		fveq2	$⊢ y = ⟨b, w⟩ \to ({2^{nd} ↾}_{F}) (y) = ({2^{nd} ↾}_{F}) (⟨b, w⟩)$
72	70 71	eqeqan12d	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \leftrightarrow ({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩))$
73		simpllr	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to x = ⟨a, v⟩$
74		simpr	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to y = ⟨b, w⟩$
75	73 74	eqeq12d	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to (x = y \leftrightarrow ⟨a, v⟩ = ⟨b, w⟩)$
76	72 75	imbi12d	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to ((({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y) \leftrightarrow (({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩) \to ⟨a, v⟩ = ⟨b, w⟩))$
77	76	imbi2d	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to ((F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y)) \leftrightarrow (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (⟨a, v⟩) = ({2^{nd} ↾}_{F}) (⟨b, w⟩) \to ⟨a, v⟩ = ⟨b, w⟩)))$
78	63 68 77	3imtr4d	$⊢ ((((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \land y = ⟨b, w⟩) \to ((F \subseteq A \times B \land (x \in F \land y \in F)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y)))$
79	78	ex	$⊢ (((a \in A \land v \in B) \land x = ⟨a, v⟩) \land (b \in A \land w \in B)) \to (y = ⟨b, w⟩ \to ((F \subseteq A \times B \land (x \in F \land y \in F)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y))))$
80	79	rexlimdvva	$⊢ ((a \in A \land v \in B) \land x = ⟨a, v⟩) \to (\exists b \in A \exists w \in B y = ⟨b, w⟩ \to ((F \subseteq A \times B \land (x \in F \land y \in F)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y))))$
81	80	ex	$⊢ (a \in A \land v \in B) \to (x = ⟨a, v⟩ \to (\exists b \in A \exists w \in B y = ⟨b, w⟩ \to ((F \subseteq A \times B \land (x \in F \land y \in F)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y)))))$
82	81	rexlimivv	$⊢ \exists a \in A \exists v \in B x = ⟨a, v⟩ \to (\exists b \in A \exists w \in B y = ⟨b, w⟩ \to ((F \subseteq A \times B \land (x \in F \land y \in F)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y))))$
83	82	imp	$⊢ (\exists a \in A \exists v \in B x = ⟨a, v⟩ \land \exists b \in A \exists w \in B y = ⟨b, w⟩) \to ((F \subseteq A \times B \land (x \in F \land y \in F)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y)))$
84	14 83	mpcom	$⊢ (F \subseteq A \times B \land (x \in F \land y \in F)) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y))$
85	84	ex	$⊢ F \subseteq A \times B \to ((x \in F \land y \in F) \to (F : A \underset{1-1}{⟶} B \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y)))$
86	85	com23	$⊢ F \subseteq A \times B \to (F : A \underset{1-1}{⟶} B \to ((x \in F \land y \in F) \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y)))$
87	7 86	mpcom	$⊢ F : A \underset{1-1}{⟶} B \to ((x \in F \land y \in F) \to (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y))$
88	87	ralrimivv	$⊢ F : A \underset{1-1}{⟶} B \to \forall x \in F \forall y \in F (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y)$
89		dff13	$⊢ ({2^{nd} ↾}_{F}) : F \underset{1-1}{⟶} B \leftrightarrow (({2^{nd} ↾}_{F}) : F ⟶ B \land \forall x \in F \forall y \in F (({2^{nd} ↾}_{F}) (x) = ({2^{nd} ↾}_{F}) (y) \to x = y))$
90	5 88 89	sylanbrc	$⊢ F : A \underset{1-1}{⟶} B \to ({2^{nd} ↾}_{F}) : F \underset{1-1}{⟶} B$
91		df-f1	$⊢ ({2^{nd} ↾}_{F}) : F \underset{1-1}{⟶} B \leftrightarrow (({2^{nd} ↾}_{F}) : F ⟶ B \land Fun {({2^{nd} ↾}_{F})}^{-1})$
92	91	simprbi	$⊢ ({2^{nd} ↾}_{F}) : F \underset{1-1}{⟶} B \to Fun {({2^{nd} ↾}_{F})}^{-1}$
93	90 92	syl	$⊢ F : A \underset{1-1}{⟶} B \to Fun {({2^{nd} ↾}_{F})}^{-1}$
94		dff1o3	$⊢ ({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F \leftrightarrow (({2^{nd} ↾}_{F}) : F \underset{onto}{⟶} ran F \land Fun {({2^{nd} ↾}_{F})}^{-1})$
95	3 93 94	sylanbrc	$⊢ F : A \underset{1-1}{⟶} B \to ({2^{nd} ↾}_{F}) : F \underset{1-1 onto}{⟶} ran F$

Metamath Proof Explorer

Theorem f1o2ndf1

Proof