f1resrcmplf1d

Description: If a function's restriction to a subclass of its domain and its restriction to the relative complement of that subclass are both one-to-one, and if the ranges of those two restrictions are disjoint, then the function is itself one-to-one. (Contributed by BTernaryTau, 28-Sep-2023)

	Ref	Expression
Hypotheses	f1resrcmplf1d.1	$⊢ φ \to C \subseteq A$
	f1resrcmplf1d.2	$⊢ φ \to F : A ⟶ B$
	f1resrcmplf1d.3	$⊢ φ \to ({F ↾}_{C}) : C \underset{1-1}{⟶} B$
	f1resrcmplf1d.4	$⊢ φ \to ({F ↾}_{(A ∖ C)}) : A ∖ C \underset{1-1}{⟶} B$
	f1resrcmplf1d.5	$⊢ φ \to F [C] \cap F [A ∖ C] = \emptyset$
Assertion	f1resrcmplf1d	$⊢ φ \to F : A \underset{1-1}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		f1resrcmplf1d.1	$⊢ φ \to C \subseteq A$
2		f1resrcmplf1d.2	$⊢ φ \to F : A ⟶ B$
3		f1resrcmplf1d.3	$⊢ φ \to ({F ↾}_{C}) : C \underset{1-1}{⟶} B$
4		f1resrcmplf1d.4	$⊢ φ \to ({F ↾}_{(A ∖ C)}) : A ∖ C \underset{1-1}{⟶} B$
5		f1resrcmplf1d.5	$⊢ φ \to F [C] \cap F [A ∖ C] = \emptyset$
6		f1resveqaeq	$⊢ (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land (x \in C \land y \in C)) \to (F (x) = F (y) \to x = y)$
7	3 6	sylan	$⊢ (φ \land (x \in C \land y \in C)) \to (F (x) = F (y) \to x = y)$
8	7	ex	$⊢ φ \to ((x \in C \land y \in C) \to (F (x) = F (y) \to x = y))$
9	1	3ad2ant1	$⊢ (φ \land (x \in C \land y \in (A ∖ C)) \land F (x) = F (y)) \to C \subseteq A$
10		difssd	$⊢ φ \to A ∖ C \subseteq A$
11	10	3ad2ant1	$⊢ (φ \land (x \in C \land y \in (A ∖ C)) \land F (x) = F (y)) \to A ∖ C \subseteq A$
12	2	3ad2ant1	$⊢ (φ \land (x \in C \land y \in (A ∖ C)) \land F (x) = F (y)) \to F : A ⟶ B$
13	5	3ad2ant1	$⊢ (φ \land (x \in C \land y \in (A ∖ C)) \land F (x) = F (y)) \to F [C] \cap F [A ∖ C] = \emptyset$
14		simp2l	$⊢ (φ \land (x \in C \land y \in (A ∖ C)) \land F (x) = F (y)) \to x \in C$
15		simp2r	$⊢ (φ \land (x \in C \land y \in (A ∖ C)) \land F (x) = F (y)) \to y \in (A ∖ C)$
16		simp3	$⊢ (φ \land (x \in C \land y \in (A ∖ C)) \land F (x) = F (y)) \to F (x) = F (y)$
17	9 11 12 13 14 15 16	f1resrcmplf1dlem	$⊢ (φ \land (x \in C \land y \in (A ∖ C)) \land F (x) = F (y)) \to x = y$
18	17	3exp	$⊢ φ \to ((x \in C \land y \in (A ∖ C)) \to (F (x) = F (y) \to x = y))$
19	10	3ad2ant1	$⊢ (φ \land (x \in (A ∖ C) \land y \in C) \land F (x) = F (y)) \to A ∖ C \subseteq A$
20	1	3ad2ant1	$⊢ (φ \land (x \in (A ∖ C) \land y \in C) \land F (x) = F (y)) \to C \subseteq A$
21	2	3ad2ant1	$⊢ (φ \land (x \in (A ∖ C) \land y \in C) \land F (x) = F (y)) \to F : A ⟶ B$
22		incom	$⊢ F [C] \cap F [A ∖ C] = F [A ∖ C] \cap F [C]$
23	22 5	eqtr3id	$⊢ φ \to F [A ∖ C] \cap F [C] = \emptyset$
24	23	3ad2ant1	$⊢ (φ \land (x \in (A ∖ C) \land y \in C) \land F (x) = F (y)) \to F [A ∖ C] \cap F [C] = \emptyset$
25		simp2l	$⊢ (φ \land (x \in (A ∖ C) \land y \in C) \land F (x) = F (y)) \to x \in (A ∖ C)$
26		simp2r	$⊢ (φ \land (x \in (A ∖ C) \land y \in C) \land F (x) = F (y)) \to y \in C$
27		simp3	$⊢ (φ \land (x \in (A ∖ C) \land y \in C) \land F (x) = F (y)) \to F (x) = F (y)$
28	19 20 21 24 25 26 27	f1resrcmplf1dlem	$⊢ (φ \land (x \in (A ∖ C) \land y \in C) \land F (x) = F (y)) \to x = y$
29	28	3exp	$⊢ φ \to ((x \in (A ∖ C) \land y \in C) \to (F (x) = F (y) \to x = y))$
30		f1resveqaeq	$⊢ (({F ↾}_{(A ∖ C)}) : A ∖ C \underset{1-1}{⟶} B \land (x \in (A ∖ C) \land y \in (A ∖ C))) \to (F (x) = F (y) \to x = y)$
31	4 30	sylan	$⊢ (φ \land (x \in (A ∖ C) \land y \in (A ∖ C))) \to (F (x) = F (y) \to x = y)$
32	31	ex	$⊢ φ \to ((x \in (A ∖ C) \land y \in (A ∖ C)) \to (F (x) = F (y) \to x = y))$
33	8 18 29 32	prsrcmpltd	$⊢ φ \to ((x \in A \land y \in A) \to (F (x) = F (y) \to x = y))$
34	33	ralrimivv	$⊢ φ \to \forall x \in A \forall y \in A (F (x) = F (y) \to x = y)$
35		dff13	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in A (F (x) = F (y) \to x = y))$
36	2 34 35	sylanbrc	$⊢ φ \to F : A \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem f1resrcmplf1d

Proof