eqfunresadj

Description: Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021)

		Ref	Expression
	Assertion	eqfunresadj	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to {F ↾}_{(X \cup \{Y\})} = {G ↾}_{(X \cup \{Y\})}$

Proof

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({F ↾}_{(X \cup \{Y\})})$
2		relres	$⊢ Rel ({G ↾}_{(X \cup \{Y\})})$
3		breq	$⊢ {F ↾}_{X} = {G ↾}_{X} \to (x ({F ↾}_{X}) y \leftrightarrow x ({G ↾}_{X}) y)$
4	3	3ad2ant2	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to (x ({F ↾}_{X}) y \leftrightarrow x ({G ↾}_{X}) y)$
5		velsn	$⊢ x \in \{Y\} \leftrightarrow x = Y$
6		simp33	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to F (Y) = G (Y)$
7	6	eqeq1d	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to (F (Y) = y \leftrightarrow G (Y) = y)$
8		simp1l	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to Fun F$
9		simp31	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to Y \in dom F$
10		funbrfvb	$⊢ (Fun F \land Y \in dom F) \to (F (Y) = y \leftrightarrow Y F y)$
11	8 9 10	syl2anc	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to (F (Y) = y \leftrightarrow Y F y)$
12		simp1r	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to Fun G$
13		simp32	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to Y \in dom G$
14		funbrfvb	$⊢ (Fun G \land Y \in dom G) \to (G (Y) = y \leftrightarrow Y G y)$
15	12 13 14	syl2anc	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to (G (Y) = y \leftrightarrow Y G y)$
16	7 11 15	3bitr3d	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to (Y F y \leftrightarrow Y G y)$
17		breq1	$⊢ x = Y \to (x F y \leftrightarrow Y F y)$
18		breq1	$⊢ x = Y \to (x G y \leftrightarrow Y G y)$
19	17 18	bibi12d	$⊢ x = Y \to ((x F y \leftrightarrow x G y) \leftrightarrow (Y F y \leftrightarrow Y G y))$
20	16 19	syl5ibrcom	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to (x = Y \to (x F y \leftrightarrow x G y))$
21	5 20	biimtrid	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to (x \in \{Y\} \to (x F y \leftrightarrow x G y))$
22	21	pm5.32d	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to ((x \in \{Y\} \land x F y) \leftrightarrow (x \in \{Y\} \land x G y))$
23		vex	$⊢ y \in V$
24	23	brresi	$⊢ x ({F ↾}_{\{Y\}}) y \leftrightarrow (x \in \{Y\} \land x F y)$
25	23	brresi	$⊢ x ({G ↾}_{\{Y\}}) y \leftrightarrow (x \in \{Y\} \land x G y)$
26	22 24 25	3bitr4g	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to (x ({F ↾}_{\{Y\}}) y \leftrightarrow x ({G ↾}_{\{Y\}}) y)$
27	4 26	orbi12d	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to ((x ({F ↾}_{X}) y \lor x ({F ↾}_{\{Y\}}) y) \leftrightarrow (x ({G ↾}_{X}) y \lor x ({G ↾}_{\{Y\}}) y))$
28		resundi	$⊢ {F ↾}_{(X \cup \{Y\})} = ({F ↾}_{X}) \cup ({F ↾}_{\{Y\}})$
29	28	breqi	$⊢ x ({F ↾}_{(X \cup \{Y\})}) y \leftrightarrow x (({F ↾}_{X}) \cup ({F ↾}_{\{Y\}})) y$
30		brun	$⊢ x (({F ↾}_{X}) \cup ({F ↾}_{\{Y\}})) y \leftrightarrow (x ({F ↾}_{X}) y \lor x ({F ↾}_{\{Y\}}) y)$
31	29 30	bitri	$⊢ x ({F ↾}_{(X \cup \{Y\})}) y \leftrightarrow (x ({F ↾}_{X}) y \lor x ({F ↾}_{\{Y\}}) y)$
32		resundi	$⊢ {G ↾}_{(X \cup \{Y\})} = ({G ↾}_{X}) \cup ({G ↾}_{\{Y\}})$
33	32	breqi	$⊢ x ({G ↾}_{(X \cup \{Y\})}) y \leftrightarrow x (({G ↾}_{X}) \cup ({G ↾}_{\{Y\}})) y$
34		brun	$⊢ x (({G ↾}_{X}) \cup ({G ↾}_{\{Y\}})) y \leftrightarrow (x ({G ↾}_{X}) y \lor x ({G ↾}_{\{Y\}}) y)$
35	33 34	bitri	$⊢ x ({G ↾}_{(X \cup \{Y\})}) y \leftrightarrow (x ({G ↾}_{X}) y \lor x ({G ↾}_{\{Y\}}) y)$
36	27 31 35	3bitr4g	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to (x ({F ↾}_{(X \cup \{Y\})}) y \leftrightarrow x ({G ↾}_{(X \cup \{Y\})}) y)$
37	1 2 36	eqbrrdiv	$⊢ ((Fun F \land Fun G) \land {F ↾}_{X} = {G ↾}_{X} \land (Y \in dom F \land Y \in dom G \land F (Y) = G (Y))) \to {F ↾}_{(X \cup \{Y\})} = {G ↾}_{(X \cup \{Y\})}$

Metamath Proof Explorer

Theorem eqfunresadj

Proof