resf1extb

Description: Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025)

		Ref	Expression
	Assertion	resf1extb	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C]) \leftrightarrow ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to F : A ⟶ B$
2		simp3	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to C \subseteq A$
3		eldifi	$⊢ X \in (A ∖ C) \to X \in A$
4	3	snssd	$⊢ X \in (A ∖ C) \to \{X\} \subseteq A$
5	4	3ad2ant2	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to \{X\} \subseteq A$
6	2 5	unssd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to C \cup \{X\} \subseteq A$
7	1 6	fssresd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B$
8	7	adantr	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])) \to ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B$
9		elun	$⊢ y \in (C \cup \{X\}) \leftrightarrow (y \in C \lor y \in \{X\})$
10		elun	$⊢ z \in (C \cup \{X\}) \leftrightarrow (z \in C \lor z \in \{X\})$
11	9 10	anbi12i	$⊢ (y \in (C \cup \{X\}) \land z \in (C \cup \{X\})) \leftrightarrow ((y \in C \lor y \in \{X\}) \land (z \in C \lor z \in \{X\}))$
12		dff14a	$⊢ ({F ↾}_{C}) : C \underset{1-1}{⟶} B \leftrightarrow (({F ↾}_{C}) : C ⟶ B \land \forall w \in C \forall x \in C (w \neq x \to ({F ↾}_{C}) (w) \neq ({F ↾}_{C}) (x)))$
13		neeq1	$⊢ w = y \to (w \neq x \leftrightarrow y \neq x)$
14		fveq2	$⊢ w = y \to ({F ↾}_{C}) (w) = ({F ↾}_{C}) (y)$
15	14	neeq1d	$⊢ w = y \to (({F ↾}_{C}) (w) \neq ({F ↾}_{C}) (x) \leftrightarrow ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (x))$
16	13 15	imbi12d	$⊢ w = y \to ((w \neq x \to ({F ↾}_{C}) (w) \neq ({F ↾}_{C}) (x)) \leftrightarrow (y \neq x \to ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (x)))$
17		neeq2	$⊢ x = z \to (y \neq x \leftrightarrow y \neq z)$
18		fveq2	$⊢ x = z \to ({F ↾}_{C}) (x) = ({F ↾}_{C}) (z)$
19	18	neeq2d	$⊢ x = z \to (({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (x) \leftrightarrow ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (z))$
20	17 19	imbi12d	$⊢ x = z \to ((y \neq x \to ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (x)) \leftrightarrow (y \neq z \to ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (z)))$
21	16 20	rspc2v	$⊢ (y \in C \land z \in C) \to (\forall w \in C \forall x \in C (w \neq x \to ({F ↾}_{C}) (w) \neq ({F ↾}_{C}) (x)) \to (y \neq z \to ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (z)))$
22		simpl	$⊢ (y \in C \land z \in C) \to y \in C$
23	22	fvresd	$⊢ (y \in C \land z \in C) \to ({F ↾}_{C}) (y) = F (y)$
24		simpr	$⊢ (y \in C \land z \in C) \to z \in C$
25	24	fvresd	$⊢ (y \in C \land z \in C) \to ({F ↾}_{C}) (z) = F (z)$
26	23 25	neeq12d	$⊢ (y \in C \land z \in C) \to (({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (z) \leftrightarrow F (y) \neq F (z))$
27	26	imbi2d	$⊢ (y \in C \land z \in C) \to ((y \neq z \to ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (z)) \leftrightarrow (y \neq z \to F (y) \neq F (z)))$
28	27	bi23imp13	$⊢ ((y \in C \land z \in C) \land (y \neq z \to ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (z)) \land y \neq z) \to F (y) \neq F (z)$
29		elun1	$⊢ y \in C \to y \in (C \cup \{X\})$
30	29	adantr	$⊢ (y \in C \land z \in C) \to y \in (C \cup \{X\})$
31	30	fvresd	$⊢ (y \in C \land z \in C) \to ({F ↾}_{(C \cup \{X\})}) (y) = F (y)$
32		elun1	$⊢ z \in C \to z \in (C \cup \{X\})$
33	32	adantl	$⊢ (y \in C \land z \in C) \to z \in (C \cup \{X\})$
34	33	fvresd	$⊢ (y \in C \land z \in C) \to ({F ↾}_{(C \cup \{X\})}) (z) = F (z)$
35	31 34	neeq12d	$⊢ (y \in C \land z \in C) \to (({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z) \leftrightarrow F (y) \neq F (z))$
36	35	3ad2ant1	$⊢ ((y \in C \land z \in C) \land (y \neq z \to ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (z)) \land y \neq z) \to (({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z) \leftrightarrow F (y) \neq F (z))$
37	28 36	mpbird	$⊢ ((y \in C \land z \in C) \land (y \neq z \to ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (z)) \land y \neq z) \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)$
38	37	3exp	$⊢ (y \in C \land z \in C) \to ((y \neq z \to ({F ↾}_{C}) (y) \neq ({F ↾}_{C}) (z)) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
39	21 38	syldc	$⊢ \forall w \in C \forall x \in C (w \neq x \to ({F ↾}_{C}) (w) \neq ({F ↾}_{C}) (x)) \to ((y \in C \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
40	39	adantl	$⊢ (({F ↾}_{C}) : C ⟶ B \land \forall w \in C \forall x \in C (w \neq x \to ({F ↾}_{C}) (w) \neq ({F ↾}_{C}) (x))) \to ((y \in C \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
41	40	a1i	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((({F ↾}_{C}) : C ⟶ B \land \forall w \in C \forall x \in C (w \neq x \to ({F ↾}_{C}) (w) \neq ({F ↾}_{C}) (x))) \to ((y \in C \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))))$
42	12 41	biimtrid	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to ((y \in C \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))))$
43	42	a1dd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to (F (X) \notin F [C] \to ((y \in C \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))))$
44	43	imp32	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])) \to ((y \in C \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
45		ffn	$⊢ F : A ⟶ B \to F Fn A$
46	45	3ad2ant1	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to F Fn A$
47	46 2	fvelimabd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (F (X) \in F [C] \leftrightarrow \exists x \in C F (x) = F (X))$
48	47	notbid	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (\neg F (X) \in F [C] \leftrightarrow \neg \exists x \in C F (x) = F (X))$
49		df-nel	$⊢ F (X) \notin F [C] \leftrightarrow \neg F (X) \in F [C]$
50		ralnex	$⊢ \forall x \in C \neg F (x) = F (X) \leftrightarrow \neg \exists x \in C F (x) = F (X)$
51	48 49 50	3bitr4g	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (F (X) \notin F [C] \leftrightarrow \forall x \in C \neg F (x) = F (X))$
52		df-ne	$⊢ F (x) \neq F (X) \leftrightarrow \neg F (x) = F (X)$
53		fveq2	$⊢ x = z \to F (x) = F (z)$
54	53	neeq1d	$⊢ x = z \to (F (x) \neq F (X) \leftrightarrow F (z) \neq F (X))$
55	52 54	bitr3id	$⊢ x = z \to (\neg F (x) = F (X) \leftrightarrow F (z) \neq F (X))$
56	55	rspcv	$⊢ z \in C \to (\forall x \in C \neg F (x) = F (X) \to F (z) \neq F (X))$
57	56	ad2antll	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to (\forall x \in C \neg F (x) = F (X) \to F (z) \neq F (X))$
58	32	ad2antll	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to z \in (C \cup \{X\})$
59	58	fvresd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to ({F ↾}_{(C \cup \{X\})}) (z) = F (z)$
60	59	eqcomd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to F (z) = ({F ↾}_{(C \cup \{X\})}) (z)$
61		elsni	$⊢ y \in \{X\} \to y = X$
62	61	eqcomd	$⊢ y \in \{X\} \to X = y$
63	62	ad2antrl	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to X = y$
64	63	fveq2d	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to F (X) = F (y)$
65		elun2	$⊢ y \in \{X\} \to y \in (C \cup \{X\})$
66	65	ad2antrl	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to y \in (C \cup \{X\})$
67	66	fvresd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to ({F ↾}_{(C \cup \{X\})}) (y) = F (y)$
68	64 67	eqtr4d	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to F (X) = ({F ↾}_{(C \cup \{X\})}) (y)$
69	60 68	neeq12d	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to (F (z) \neq F (X) \leftrightarrow ({F ↾}_{(C \cup \{X\})}) (z) \neq ({F ↾}_{(C \cup \{X\})}) (y))$
70	69	biimpa	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \land F (z) \neq F (X)) \to ({F ↾}_{(C \cup \{X\})}) (z) \neq ({F ↾}_{(C \cup \{X\})}) (y)$
71	70	necomd	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \land F (z) \neq F (X)) \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)$
72	71	a1d	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \land F (z) \neq F (X)) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))$
73	72	ex	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to (F (z) \neq F (X) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
74	57 73	syld	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to (\forall x \in C \neg F (x) = F (X) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
75	74	a1d	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in \{X\} \land z \in C)) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to (\forall x \in C \neg F (x) = F (X) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))))$
76	75	ex	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((y \in \{X\} \land z \in C) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to (\forall x \in C \neg F (x) = F (X) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))))$
77	76	com24	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (\forall x \in C \neg F (x) = F (X) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to ((y \in \{X\} \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))))$
78	51 77	sylbid	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (F (X) \notin F [C] \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to ((y \in \{X\} \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))))$
79	78	impcomd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C]) \to ((y \in \{X\} \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))))$
80	79	imp	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])) \to ((y \in \{X\} \land z \in C) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
81		fveq2	$⊢ x = y \to F (x) = F (y)$
82	81	neeq1d	$⊢ x = y \to (F (x) \neq F (X) \leftrightarrow F (y) \neq F (X))$
83	52 82	bitr3id	$⊢ x = y \to (\neg F (x) = F (X) \leftrightarrow F (y) \neq F (X))$
84	83	rspcv	$⊢ y \in C \to (\forall x \in C \neg F (x) = F (X) \to F (y) \neq F (X))$
85	84	ad2antrl	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to (\forall x \in C \neg F (x) = F (X) \to F (y) \neq F (X))$
86	29	ad2antrl	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to y \in (C \cup \{X\})$
87	86	fvresd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to ({F ↾}_{(C \cup \{X\})}) (y) = F (y)$
88	87	eqcomd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to F (y) = ({F ↾}_{(C \cup \{X\})}) (y)$
89		elsni	$⊢ z \in \{X\} \to z = X$
90	89	eqcomd	$⊢ z \in \{X\} \to X = z$
91	90	ad2antll	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to X = z$
92	91	fveq2d	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to F (X) = F (z)$
93		elun2	$⊢ z \in \{X\} \to z \in (C \cup \{X\})$
94	93	ad2antll	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to z \in (C \cup \{X\})$
95	94	fvresd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to ({F ↾}_{(C \cup \{X\})}) (z) = F (z)$
96	92 95	eqtr4d	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to F (X) = ({F ↾}_{(C \cup \{X\})}) (z)$
97	88 96	neeq12d	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to (F (y) \neq F (X) \leftrightarrow ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))$
98	97	biimpd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to (F (y) \neq F (X) \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))$
99	98	a1dd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to (F (y) \neq F (X) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
100	85 99	syld	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to (\forall x \in C \neg F (x) = F (X) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
101	100	a1d	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (y \in C \land z \in \{X\})) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to (\forall x \in C \neg F (x) = F (X) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))))$
102	101	ex	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((y \in C \land z \in \{X\}) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to (\forall x \in C \neg F (x) = F (X) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))))$
103	102	com24	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (\forall x \in C \neg F (x) = F (X) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to ((y \in C \land z \in \{X\}) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))))$
104	51 103	sylbid	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (F (X) \notin F [C] \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \to ((y \in C \land z \in \{X\}) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))))$
105	104	impcomd	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C]) \to ((y \in C \land z \in \{X\}) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))))$
106	105	imp	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])) \to ((y \in C \land z \in \{X\}) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
107		velsn	$⊢ y \in \{X\} \leftrightarrow y = X$
108		velsn	$⊢ z \in \{X\} \leftrightarrow z = X$
109		eqtr3	$⊢ (y = X \land z = X) \to y = z$
110		eqneqall	$⊢ y = z \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))$
111	109 110	syl	$⊢ (y = X \land z = X) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))$
112	107 108 111	syl2anb	$⊢ (y \in \{X\} \land z \in \{X\}) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))$
113	112	a1i	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])) \to ((y \in \{X\} \land z \in \{X\}) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
114	44 80 106 113	ccased	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])) \to (((y \in C \lor y \in \{X\}) \land (z \in C \lor z \in \{X\})) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
115	11 114	biimtrid	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])) \to ((y \in (C \cup \{X\}) \land z \in (C \cup \{X\})) \to (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
116	115	ralrimivv	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])) \to \forall y \in (C \cup \{X\}) \forall z \in (C \cup \{X\}) (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))$
117		dff14a	$⊢ ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B \leftrightarrow (({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B \land \forall y \in (C \cup \{X\}) \forall z \in (C \cup \{X\}) (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
118	8 116 117	sylanbrc	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])) \to ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B$
119		fssres	$⊢ (F : A ⟶ B \land C \subseteq A) \to ({F ↾}_{C}) : C ⟶ B$
120	119	3adant2	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ({F ↾}_{C}) : C ⟶ B$
121	120	adantr	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \to ({F ↾}_{C}) : C ⟶ B$
122		df-f1	$⊢ ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B \leftrightarrow (({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B \land Fun {({F ↾}_{(C \cup \{X\})})}^{-1})$
123		funres11	$⊢ Fun {({F ↾}_{(C \cup \{X\})})}^{-1} \to Fun {({({F ↾}_{(C \cup \{X\})}) ↾}_{C})}^{-1}$
124	122 123	simplbiim	$⊢ ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B \to Fun {({({F ↾}_{(C \cup \{X\})}) ↾}_{C})}^{-1}$
125	124	adantl	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \to Fun {({({F ↾}_{(C \cup \{X\})}) ↾}_{C})}^{-1}$
126		ssun1	$⊢ C \subseteq C \cup \{X\}$
127	126	resabs1i	$⊢ {({F ↾}_{(C \cup \{X\})}) ↾}_{C} = {F ↾}_{C}$
128	127	eqcomi	$⊢ {F ↾}_{C} = {({F ↾}_{(C \cup \{X\})}) ↾}_{C}$
129	128	cnveqi	$⊢ {({F ↾}_{C})}^{-1} = {({({F ↾}_{(C \cup \{X\})}) ↾}_{C})}^{-1}$
130	129	funeqi	$⊢ Fun {({F ↾}_{C})}^{-1} \leftrightarrow Fun {({({F ↾}_{(C \cup \{X\})}) ↾}_{C})}^{-1}$
131	125 130	sylibr	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \to Fun {({F ↾}_{C})}^{-1}$
132		df-f1	$⊢ ({F ↾}_{C}) : C \underset{1-1}{⟶} B \leftrightarrow (({F ↾}_{C}) : C ⟶ B \land Fun {({F ↾}_{C})}^{-1})$
133	121 131 132	sylanbrc	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \to ({F ↾}_{C}) : C \underset{1-1}{⟶} B$
134		elun1	$⊢ x \in C \to x \in (C \cup \{X\})$
135		snidg	$⊢ X \in (A ∖ C) \to X \in \{X\}$
136	135	3ad2ant2	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to X \in \{X\}$
137		elun2	$⊢ X \in \{X\} \to X \in (C \cup \{X\})$
138	136 137	syl	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to X \in (C \cup \{X\})$
139		neeq1	$⊢ y = x \to (y \neq z \leftrightarrow x \neq z)$
140		fveq2	$⊢ y = x \to ({F ↾}_{(C \cup \{X\})}) (y) = ({F ↾}_{(C \cup \{X\})}) (x)$
141	140	neeq1d	$⊢ y = x \to (({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z) \leftrightarrow ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (z))$
142	139 141	imbi12d	$⊢ y = x \to ((y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)) \leftrightarrow (x \neq z \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (z)))$
143		neeq2	$⊢ z = X \to (x \neq z \leftrightarrow x \neq X)$
144		fveq2	$⊢ z = X \to ({F ↾}_{(C \cup \{X\})}) (z) = ({F ↾}_{(C \cup \{X\})}) (X)$
145	144	neeq2d	$⊢ z = X \to (({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (z) \leftrightarrow ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X))$
146	143 145	imbi12d	$⊢ z = X \to ((x \neq z \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (z)) \leftrightarrow (x \neq X \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X)))$
147	142 146	rspc2v	$⊢ (x \in (C \cup \{X\}) \land X \in (C \cup \{X\})) \to (\forall y \in (C \cup \{X\}) \forall z \in (C \cup \{X\}) (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)) \to (x \neq X \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X)))$
148	134 138 147	syl2anr	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \to (\forall y \in (C \cup \{X\}) \forall z \in (C \cup \{X\}) (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)) \to (x \neq X \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X)))$
149	148	adantr	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B) \to (\forall y \in (C \cup \{X\}) \forall z \in (C \cup \{X\}) (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)) \to (x \neq X \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X)))$
150		eldifn	$⊢ X \in (A ∖ C) \to \neg X \in C$
151		nelelne	$⊢ \neg X \in C \to (x \in C \to x \neq X)$
152	150 151	syl	$⊢ X \in (A ∖ C) \to (x \in C \to x \neq X)$
153	152	3ad2ant2	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to (x \in C \to x \neq X)$
154	153	imp	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \to x \neq X$
155	154	adantr	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B) \to x \neq X$
156		pm2.27	$⊢ x \neq X \to ((x \neq X \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X)) \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X))$
157	155 156	syl	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B) \to ((x \neq X \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X)) \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X))$
158	134	adantl	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \to x \in (C \cup \{X\})$
159	158	adantr	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B) \to x \in (C \cup \{X\})$
160	159	fvresd	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B) \to ({F ↾}_{(C \cup \{X\})}) (x) = F (x)$
161	135 137	syl	$⊢ X \in (A ∖ C) \to X \in (C \cup \{X\})$
162	161	3ad2ant2	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to X \in (C \cup \{X\})$
163	162	adantr	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \to X \in (C \cup \{X\})$
164	163	fvresd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \to ({F ↾}_{(C \cup \{X\})}) (X) = F (X)$
165	164	adantr	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B) \to ({F ↾}_{(C \cup \{X\})}) (X) = F (X)$
166	160 165	neeq12d	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B) \to (({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X) \leftrightarrow F (x) \neq F (X))$
167	157 166	sylibd	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B) \to ((x \neq X \to ({F ↾}_{(C \cup \{X\})}) (x) \neq ({F ↾}_{(C \cup \{X\})}) (X)) \to F (x) \neq F (X))$
168	149 167	syld	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B) \to (\forall y \in (C \cup \{X\}) \forall z \in (C \cup \{X\}) (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z)) \to F (x) \neq F (X))$
169	168	expimpd	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \to ((({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} ⟶ B \land \forall y \in (C \cup \{X\}) \forall z \in (C \cup \{X\}) (y \neq z \to ({F ↾}_{(C \cup \{X\})}) (y) \neq ({F ↾}_{(C \cup \{X\})}) (z))) \to F (x) \neq F (X))$
170	117 169	biimtrid	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land x \in C) \to (({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B \to F (x) \neq F (X))$
171	170	impancom	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \to (x \in C \to F (x) \neq F (X))$
172	171	imp	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \land x \in C) \to F (x) \neq F (X)$
173	172	neneqd	$⊢ (((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \land x \in C) \to \neg F (x) = F (X)$
174	173	ralrimiva	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \to \forall x \in C \neg F (x) = F (X)$
175	51	adantr	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \to (F (X) \notin F [C] \leftrightarrow \forall x \in C \neg F (x) = F (X))$
176	174 175	mpbird	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \to F (X) \notin F [C]$
177	133 176	jca	$⊢ ((F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \land ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B) \to (({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C])$
178	118 177	impbida	$⊢ (F : A ⟶ B \land X \in (A ∖ C) \land C \subseteq A) \to ((({F ↾}_{C}) : C \underset{1-1}{⟶} B \land F (X) \notin F [C]) \leftrightarrow ({F ↾}_{(C \cup \{X\})}) : C \cup \{X\} \underset{1-1}{⟶} B)$

Metamath Proof Explorer

Theorem resf1extb

Proof