resf1o

Description: Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017)

	Ref	Expression
Hypotheses	resf1o.1	$⊢ X = \{f \in (B^{A}) \| f^{-1} [B ∖ \{Z\}] \subseteq C\}$
	resf1o.2	$⊢ F = (f \in X ⟼ {f ↾}_{C})$
Assertion	resf1o	$⊢ ((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \to F : X \underset{1-1 onto}{⟶} B^{C}$

Proof

Step	Hyp	Ref	Expression
1		resf1o.1	$⊢ X = \{f \in (B^{A}) \| f^{-1} [B ∖ \{Z\}] \subseteq C\}$
2		resf1o.2	$⊢ F = (f \in X ⟼ {f ↾}_{C})$
3		resexg	$⊢ f \in X \to {f ↾}_{C} \in V$
4	3	adantl	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land f \in X) \to {f ↾}_{C} \in V$
5		simpr	$⊢ ((A \in V \land B \in W \land C \subseteq A) \land g \in (B^{C})) \to g \in (B^{C})$
6		difexg	$⊢ A \in V \to A ∖ C \in V$
7	6	3ad2ant1	$⊢ (A \in V \land B \in W \land C \subseteq A) \to A ∖ C \in V$
8		snex	$⊢ \{Z\} \in V$
9		xpexg	$⊢ (A ∖ C \in V \land \{Z\} \in V) \to (A ∖ C) \times \{Z\} \in V$
10	7 8 9	sylancl	$⊢ (A \in V \land B \in W \land C \subseteq A) \to (A ∖ C) \times \{Z\} \in V$
11	10	adantr	$⊢ ((A \in V \land B \in W \land C \subseteq A) \land g \in (B^{C})) \to (A ∖ C) \times \{Z\} \in V$
12		unexg	$⊢ (g \in (B^{C}) \land (A ∖ C) \times \{Z\} \in V) \to g \cup ((A ∖ C) \times \{Z\}) \in V$
13	5 11 12	syl2anc	$⊢ ((A \in V \land B \in W \land C \subseteq A) \land g \in (B^{C})) \to g \cup ((A ∖ C) \times \{Z\}) \in V$
14	13	adantlr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land g \in (B^{C})) \to g \cup ((A ∖ C) \times \{Z\}) \in V$
15	1	reqabi	$⊢ f \in X \leftrightarrow (f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C)$
16	15	anbi1i	$⊢ (f \in X \land g = {f ↾}_{C}) \leftrightarrow ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})$
17		simprr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to g = {f ↾}_{C}$
18		simprll	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to f \in (B^{A})$
19		elmapi	$⊢ f \in (B^{A}) \to f : A ⟶ B$
20	18 19	syl	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to f : A ⟶ B$
21		simp3	$⊢ (A \in V \land B \in W \land C \subseteq A) \to C \subseteq A$
22	21	ad2antrr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to C \subseteq A$
23	20 22	fssresd	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to ({f ↾}_{C}) : C ⟶ B$
24		simp2	$⊢ (A \in V \land B \in W \land C \subseteq A) \to B \in W$
25		simp1	$⊢ (A \in V \land B \in W \land C \subseteq A) \to A \in V$
26	25 21	ssexd	$⊢ (A \in V \land B \in W \land C \subseteq A) \to C \in V$
27		elmapg	$⊢ (B \in W \land C \in V) \to ({f ↾}_{C} \in (B^{C}) \leftrightarrow ({f ↾}_{C}) : C ⟶ B)$
28	24 26 27	syl2anc	$⊢ (A \in V \land B \in W \land C \subseteq A) \to ({f ↾}_{C} \in (B^{C}) \leftrightarrow ({f ↾}_{C}) : C ⟶ B)$
29	28	ad2antrr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to ({f ↾}_{C} \in (B^{C}) \leftrightarrow ({f ↾}_{C}) : C ⟶ B)$
30	23 29	mpbird	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to {f ↾}_{C} \in (B^{C})$
31	17 30	eqeltrd	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to g \in (B^{C})$
32		undif	$⊢ C \subseteq A \leftrightarrow C \cup (A ∖ C) = A$
33	32	biimpi	$⊢ C \subseteq A \to C \cup (A ∖ C) = A$
34	33	reseq2d	$⊢ C \subseteq A \to {f ↾}_{(C \cup (A ∖ C))} = {f ↾}_{A}$
35	22 34	syl	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to {f ↾}_{(C \cup (A ∖ C))} = {f ↾}_{A}$
36		ffn	$⊢ f : A ⟶ B \to f Fn A$
37		fnresdm	$⊢ f Fn A \to {f ↾}_{A} = f$
38	20 36 37	3syl	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to {f ↾}_{A} = f$
39	35 38	eqtr2d	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to f = {f ↾}_{(C \cup (A ∖ C))}$
40		resundi	$⊢ {f ↾}_{(C \cup (A ∖ C))} = ({f ↾}_{C}) \cup ({f ↾}_{(A ∖ C)})$
41	39 40	eqtrdi	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to f = ({f ↾}_{C}) \cup ({f ↾}_{(A ∖ C)})$
42	17	eqcomd	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to {f ↾}_{C} = g$
43		simprlr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to f^{-1} [B ∖ \{Z\}] \subseteq C$
44	25	ad2antrr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to A \in V$
45		simplr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to Z \in B$
46		eqid	$⊢ B ∖ \{Z\} = B ∖ \{Z\}$
47	46	ffs2	$⊢ (A \in V \land Z \in B \land f : A ⟶ B) \to f supp Z = f^{-1} [B ∖ \{Z\}]$
48	44 45 20 47	syl3anc	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to f supp Z = f^{-1} [B ∖ \{Z\}]$
49		sseqin2	$⊢ C \subseteq A \leftrightarrow A \cap C = C$
50	49	biimpi	$⊢ C \subseteq A \to A \cap C = C$
51	22 50	syl	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to A \cap C = C$
52	43 48 51	3sstr4d	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to f supp Z \subseteq A \cap C$
53		simpl	$⊢ (f \in (B^{A}) \land Z \in B) \to f \in (B^{A})$
54	53 19 36	3syl	$⊢ (f \in (B^{A}) \land Z \in B) \to f Fn A$
55		inundif	$⊢ (A \cap C) \cup (A ∖ C) = A$
56	55	fneq2i	$⊢ f Fn ((A \cap C) \cup (A ∖ C)) \leftrightarrow f Fn A$
57	54 56	sylibr	$⊢ (f \in (B^{A}) \land Z \in B) \to f Fn ((A \cap C) \cup (A ∖ C))$
58		vex	$⊢ f \in V$
59	58	a1i	$⊢ (f \in (B^{A}) \land Z \in B) \to f \in V$
60		simpr	$⊢ (f \in (B^{A}) \land Z \in B) \to Z \in B$
61		inindif	$⊢ (A \cap C) \cap (A ∖ C) = \emptyset$
62	61	a1i	$⊢ (f \in (B^{A}) \land Z \in B) \to (A \cap C) \cap (A ∖ C) = \emptyset$
63		fnsuppres	$⊢ (f Fn ((A \cap C) \cup (A ∖ C)) \land (f \in V \land Z \in B) \land (A \cap C) \cap (A ∖ C) = \emptyset) \to (f supp Z \subseteq A \cap C \leftrightarrow {f ↾}_{(A ∖ C)} = (A ∖ C) \times \{Z\})$
64	57 59 60 62 63	syl121anc	$⊢ (f \in (B^{A}) \land Z \in B) \to (f supp Z \subseteq A \cap C \leftrightarrow {f ↾}_{(A ∖ C)} = (A ∖ C) \times \{Z\})$
65	18 45 64	syl2anc	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to (f supp Z \subseteq A \cap C \leftrightarrow {f ↾}_{(A ∖ C)} = (A ∖ C) \times \{Z\})$
66	52 65	mpbid	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to {f ↾}_{(A ∖ C)} = (A ∖ C) \times \{Z\}$
67	42 66	uneq12d	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to ({f ↾}_{C}) \cup ({f ↾}_{(A ∖ C)}) = g \cup ((A ∖ C) \times \{Z\})$
68	41 67	eqtrd	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to f = g \cup ((A ∖ C) \times \{Z\})$
69	31 68	jca	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})) \to (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))$
70	24	ad2antrr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to B \in W$
71	25	ad2antrr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to A \in V$
72		elmapi	$⊢ g \in (B^{C}) \to g : C ⟶ B$
73	72	ad2antrl	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to g : C ⟶ B$
74		simplr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to Z \in B$
75		fconst6g	$⊢ Z \in B \to ((A ∖ C) \times \{Z\}) : A ∖ C ⟶ B$
76	74 75	syl	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to ((A ∖ C) \times \{Z\}) : A ∖ C ⟶ B$
77		disjdif	$⊢ C \cap (A ∖ C) = \emptyset$
78	77	a1i	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to C \cap (A ∖ C) = \emptyset$
79		fun2	$⊢ ((g : C ⟶ B \land ((A ∖ C) \times \{Z\}) : A ∖ C ⟶ B) \land C \cap (A ∖ C) = \emptyset) \to (g \cup ((A ∖ C) \times \{Z\})) : C \cup (A ∖ C) ⟶ B$
80	73 76 78 79	syl21anc	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to (g \cup ((A ∖ C) \times \{Z\})) : C \cup (A ∖ C) ⟶ B$
81		simprr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to f = g \cup ((A ∖ C) \times \{Z\})$
82	81	eqcomd	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to g \cup ((A ∖ C) \times \{Z\}) = f$
83	21	ad2antrr	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to C \subseteq A$
84	83 33	syl	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to C \cup (A ∖ C) = A$
85	82 84	feq12d	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to ((g \cup ((A ∖ C) \times \{Z\})) : C \cup (A ∖ C) ⟶ B \leftrightarrow f : A ⟶ B)$
86	80 85	mpbid	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to f : A ⟶ B$
87		elmapg	$⊢ (B \in W \land A \in V) \to (f \in (B^{A}) \leftrightarrow f : A ⟶ B)$
88	87	biimpar	$⊢ ((B \in W \land A \in V) \land f : A ⟶ B) \to f \in (B^{A})$
89	70 71 86 88	syl21anc	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to f \in (B^{A})$
90	71 74 86 47	syl3anc	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to f supp Z = f^{-1} [B ∖ \{Z\}]$
91	81	adantr	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to f = g \cup ((A ∖ C) \times \{Z\})$
92	91	fveq1d	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to f (x) = (g \cup ((A ∖ C) \times \{Z\})) (x)$
93	73	adantr	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to g : C ⟶ B$
94	93	ffnd	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to g Fn C$
95		fconstg	$⊢ Z \in B \to ((A ∖ C) \times \{Z\}) : A ∖ C ⟶ \{Z\}$
96	95	ad3antlr	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to ((A ∖ C) \times \{Z\}) : A ∖ C ⟶ \{Z\}$
97	96	ffnd	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to ((A ∖ C) \times \{Z\}) Fn (A ∖ C)$
98	77	a1i	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to C \cap (A ∖ C) = \emptyset$
99		simpr	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to x \in (A ∖ C)$
100		fvun2	$⊢ (g Fn C \land ((A ∖ C) \times \{Z\}) Fn (A ∖ C) \land (C \cap (A ∖ C) = \emptyset \land x \in (A ∖ C))) \to (g \cup ((A ∖ C) \times \{Z\})) (x) = ((A ∖ C) \times \{Z\}) (x)$
101	94 97 98 99 100	syl112anc	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to (g \cup ((A ∖ C) \times \{Z\})) (x) = ((A ∖ C) \times \{Z\}) (x)$
102		fvconst	$⊢ (((A ∖ C) \times \{Z\}) : A ∖ C ⟶ \{Z\} \land x \in (A ∖ C)) \to ((A ∖ C) \times \{Z\}) (x) = Z$
103	96 99 102	syl2anc	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to ((A ∖ C) \times \{Z\}) (x) = Z$
104	92 101 103	3eqtrd	$⊢ ((((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \land x \in (A ∖ C)) \to f (x) = Z$
105	86 104	suppss	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to f supp Z \subseteq C$
106	90 105	eqsstrrd	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to f^{-1} [B ∖ \{Z\}] \subseteq C$
107	81	reseq1d	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to {f ↾}_{C} = {(g \cup ((A ∖ C) \times \{Z\})) ↾}_{C}$
108		res0	$⊢ {((A ∖ C) \times \{Z\}) ↾}_{\emptyset} = \emptyset$
109		res0	$⊢ {g ↾}_{\emptyset} = \emptyset$
110	108 109	eqtr4i	$⊢ {((A ∖ C) \times \{Z\}) ↾}_{\emptyset} = {g ↾}_{\emptyset}$
111	77	reseq2i	$⊢ {((A ∖ C) \times \{Z\}) ↾}_{(C \cap (A ∖ C))} = {((A ∖ C) \times \{Z\}) ↾}_{\emptyset}$
112	77	reseq2i	$⊢ {g ↾}_{(C \cap (A ∖ C))} = {g ↾}_{\emptyset}$
113	110 111 112	3eqtr4ri	$⊢ {g ↾}_{(C \cap (A ∖ C))} = {((A ∖ C) \times \{Z\}) ↾}_{(C \cap (A ∖ C))}$
114	113	a1i	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to {g ↾}_{(C \cap (A ∖ C))} = {((A ∖ C) \times \{Z\}) ↾}_{(C \cap (A ∖ C))}$
115		fresaunres1	$⊢ (g : C ⟶ B \land ((A ∖ C) \times \{Z\}) : A ∖ C ⟶ B \land {g ↾}_{(C \cap (A ∖ C))} = {((A ∖ C) \times \{Z\}) ↾}_{(C \cap (A ∖ C))}) \to {(g \cup ((A ∖ C) \times \{Z\})) ↾}_{C} = g$
116	73 76 114 115	syl3anc	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to {(g \cup ((A ∖ C) \times \{Z\})) ↾}_{C} = g$
117	107 116	eqtr2d	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to g = {f ↾}_{C}$
118	89 106 117	jca31	$⊢ (((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \land (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\}))) \to ((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C})$
119	69 118	impbida	$⊢ ((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \to (((f \in (B^{A}) \land f^{-1} [B ∖ \{Z\}] \subseteq C) \land g = {f ↾}_{C}) \leftrightarrow (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\})))$
120	16 119	bitrid	$⊢ ((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \to ((f \in X \land g = {f ↾}_{C}) \leftrightarrow (g \in (B^{C}) \land f = g \cup ((A ∖ C) \times \{Z\})))$
121	2 4 14 120	f1od	$⊢ ((A \in V \land B \in W \land C \subseteq A) \land Z \in B) \to F : X \underset{1-1 onto}{⟶} B^{C}$

Metamath Proof Explorer

Theorem resf1o

Proof