hashf1lem1

Description: Lemma for hashf1 . (Contributed by Mario Carneiro, 17-Apr-2015) (Proof shortened by AV, 14-Aug-2024)

	Ref	Expression
Hypotheses	hashf1lem2.1	$⊢ φ \to A \in Fin$
	hashf1lem2.2	$⊢ φ \to B \in Fin$
	hashf1lem2.3	$⊢ φ \to \neg z \in A$
	hashf1lem2.4	$⊢ φ \to \|A\| + 1 \leq \|B\|$
	hashf1lem1.5	$⊢ φ \to F : A \underset{1-1}{⟶} B$
Assertion	hashf1lem1	$⊢ φ \to \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \approx (B ∖ ran F)$

Proof

Step	Hyp	Ref	Expression
1		hashf1lem2.1	$⊢ φ \to A \in Fin$
2		hashf1lem2.2	$⊢ φ \to B \in Fin$
3		hashf1lem2.3	$⊢ φ \to \neg z \in A$
4		hashf1lem2.4	$⊢ φ \to \|A\| + 1 \leq \|B\|$
5		hashf1lem1.5	$⊢ φ \to F : A \underset{1-1}{⟶} B$
6		f1setex	$⊢ B \in Fin \to \{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\} \in V$
7	2 6	syl	$⊢ φ \to \{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\} \in V$
8		abanssr	$⊢ \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq \{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}$
9	8	a1i	$⊢ φ \to \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq \{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}$
10	7 9	ssexd	$⊢ φ \to \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in V$
11	2	difexd	$⊢ φ \to B ∖ ran F \in V$
12		vex	$⊢ g \in V$
13		reseq1	$⊢ f = g \to {f ↾}_{A} = {g ↾}_{A}$
14	13	eqeq1d	$⊢ f = g \to ({f ↾}_{A} = F \leftrightarrow {g ↾}_{A} = F)$
15		f1eq1	$⊢ f = g \to (f : A \cup \{z\} \underset{1-1}{⟶} B \leftrightarrow g : A \cup \{z\} \underset{1-1}{⟶} B)$
16	14 15	anbi12d	$⊢ f = g \to (({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B) \leftrightarrow ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B))$
17	12 16	elab	$⊢ g \in \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \leftrightarrow ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)$
18		f1f	$⊢ g : A \cup \{z\} \underset{1-1}{⟶} B \to g : A \cup \{z\} ⟶ B$
19	18	ad2antll	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g : A \cup \{z\} ⟶ B$
20		ssun2	$⊢ \{z\} \subseteq A \cup \{z\}$
21		vex	$⊢ z \in V$
22	21	snss	$⊢ z \in (A \cup \{z\}) \leftrightarrow \{z\} \subseteq A \cup \{z\}$
23	20 22	mpbir	$⊢ z \in (A \cup \{z\})$
24		ffvelrn	$⊢ (g : A \cup \{z\} ⟶ B \land z \in (A \cup \{z\})) \to g (z) \in B$
25	19 23 24	sylancl	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g (z) \in B$
26	3	adantr	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to \neg z \in A$
27		df-ima	$⊢ g [A] = ran ({g ↾}_{A})$
28		simprl	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to {g ↾}_{A} = F$
29	28	rneqd	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to ran ({g ↾}_{A}) = ran F$
30	27 29	eqtrid	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g [A] = ran F$
31	30	eleq2d	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to (g (z) \in g [A] \leftrightarrow g (z) \in ran F)$
32		simprr	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g : A \cup \{z\} \underset{1-1}{⟶} B$
33	23	a1i	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to z \in (A \cup \{z\})$
34		ssun1	$⊢ A \subseteq A \cup \{z\}$
35	34	a1i	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to A \subseteq A \cup \{z\}$
36		f1elima	$⊢ (g : A \cup \{z\} \underset{1-1}{⟶} B \land z \in (A \cup \{z\}) \land A \subseteq A \cup \{z\}) \to (g (z) \in g [A] \leftrightarrow z \in A)$
37	32 33 35 36	syl3anc	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to (g (z) \in g [A] \leftrightarrow z \in A)$
38	31 37	bitr3d	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to (g (z) \in ran F \leftrightarrow z \in A)$
39	26 38	mtbird	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to \neg g (z) \in ran F$
40	25 39	eldifd	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g (z) \in (B ∖ ran F)$
41	40	ex	$⊢ φ \to (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \to g (z) \in (B ∖ ran F))$
42	17 41	syl5bi	$⊢ φ \to (g \in \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \to g (z) \in (B ∖ ran F))$
43		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
44	5 43	syl	$⊢ φ \to F : A ⟶ B$
45	44	adantr	$⊢ (φ \land x \in (B ∖ ran F)) \to F : A ⟶ B$
46		vex	$⊢ x \in V$
47	21 46	f1osn	$⊢ \{⟨z, x⟩\} : \{z\} \underset{1-1 onto}{⟶} \{x\}$
48		f1of	$⊢ \{⟨z, x⟩\} : \{z\} \underset{1-1 onto}{⟶} \{x\} \to \{⟨z, x⟩\} : \{z\} ⟶ \{x\}$
49	47 48	ax-mp	$⊢ \{⟨z, x⟩\} : \{z\} ⟶ \{x\}$
50		eldifi	$⊢ x \in (B ∖ ran F) \to x \in B$
51	50	adantl	$⊢ (φ \land x \in (B ∖ ran F)) \to x \in B$
52	51	snssd	$⊢ (φ \land x \in (B ∖ ran F)) \to \{x\} \subseteq B$
53		fss	$⊢ (\{⟨z, x⟩\} : \{z\} ⟶ \{x\} \land \{x\} \subseteq B) \to \{⟨z, x⟩\} : \{z\} ⟶ B$
54	49 52 53	sylancr	$⊢ (φ \land x \in (B ∖ ran F)) \to \{⟨z, x⟩\} : \{z\} ⟶ B$
55		res0	$⊢ {F ↾}_{\emptyset} = \emptyset$
56		res0	$⊢ {\{⟨z, x⟩\} ↾}_{\emptyset} = \emptyset$
57	55 56	eqtr4i	$⊢ {F ↾}_{\emptyset} = {\{⟨z, x⟩\} ↾}_{\emptyset}$
58		disjsn	$⊢ A \cap \{z\} = \emptyset \leftrightarrow \neg z \in A$
59	3 58	sylibr	$⊢ φ \to A \cap \{z\} = \emptyset$
60	59	adantr	$⊢ (φ \land x \in (B ∖ ran F)) \to A \cap \{z\} = \emptyset$
61	60	reseq2d	$⊢ (φ \land x \in (B ∖ ran F)) \to {F ↾}_{(A \cap \{z\})} = {F ↾}_{\emptyset}$
62	60	reseq2d	$⊢ (φ \land x \in (B ∖ ran F)) \to {\{⟨z, x⟩\} ↾}_{(A \cap \{z\})} = {\{⟨z, x⟩\} ↾}_{\emptyset}$
63	57 61 62	3eqtr4a	$⊢ (φ \land x \in (B ∖ ran F)) \to {F ↾}_{(A \cap \{z\})} = {\{⟨z, x⟩\} ↾}_{(A \cap \{z\})}$
64		fresaunres1	$⊢ (F : A ⟶ B \land \{⟨z, x⟩\} : \{z\} ⟶ B \land {F ↾}_{(A \cap \{z\})} = {\{⟨z, x⟩\} ↾}_{(A \cap \{z\})}) \to {(F \cup \{⟨z, x⟩\}) ↾}_{A} = F$
65	45 54 63 64	syl3anc	$⊢ (φ \land x \in (B ∖ ran F)) \to {(F \cup \{⟨z, x⟩\}) ↾}_{A} = F$
66		f1f1orn	$⊢ F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} ran F$
67	5 66	syl	$⊢ φ \to F : A \underset{1-1 onto}{⟶} ran F$
68	67	adantr	$⊢ (φ \land x \in (B ∖ ran F)) \to F : A \underset{1-1 onto}{⟶} ran F$
69	47	a1i	$⊢ (φ \land x \in (B ∖ ran F)) \to \{⟨z, x⟩\} : \{z\} \underset{1-1 onto}{⟶} \{x\}$
70		eldifn	$⊢ x \in (B ∖ ran F) \to \neg x \in ran F$
71	70	adantl	$⊢ (φ \land x \in (B ∖ ran F)) \to \neg x \in ran F$
72		disjsn	$⊢ ran F \cap \{x\} = \emptyset \leftrightarrow \neg x \in ran F$
73	71 72	sylibr	$⊢ (φ \land x \in (B ∖ ran F)) \to ran F \cap \{x\} = \emptyset$
74		f1oun	$⊢ ((F : A \underset{1-1 onto}{⟶} ran F \land \{⟨z, x⟩\} : \{z\} \underset{1-1 onto}{⟶} \{x\}) \land (A \cap \{z\} = \emptyset \land ran F \cap \{x\} = \emptyset)) \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1 onto}{⟶} ran F \cup \{x\}$
75	68 69 60 73 74	syl22anc	$⊢ (φ \land x \in (B ∖ ran F)) \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1 onto}{⟶} ran F \cup \{x\}$
76		f1of1	$⊢ (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1 onto}{⟶} ran F \cup \{x\} \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} ran F \cup \{x\}$
77	75 76	syl	$⊢ (φ \land x \in (B ∖ ran F)) \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} ran F \cup \{x\}$
78	45	frnd	$⊢ (φ \land x \in (B ∖ ran F)) \to ran F \subseteq B$
79	78 52	unssd	$⊢ (φ \land x \in (B ∖ ran F)) \to ran F \cup \{x\} \subseteq B$
80		f1ss	$⊢ ((F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} ran F \cup \{x\} \land ran F \cup \{x\} \subseteq B) \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} B$
81	77 79 80	syl2anc	$⊢ (φ \land x \in (B ∖ ran F)) \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} B$
82	44 1	fexd	$⊢ φ \to F \in V$
83	82	adantr	$⊢ (φ \land x \in (B ∖ ran F)) \to F \in V$
84		snex	$⊢ \{⟨z, x⟩\} \in V$
85		unexg	$⊢ (F \in V \land \{⟨z, x⟩\} \in V) \to F \cup \{⟨z, x⟩\} \in V$
86	83 84 85	sylancl	$⊢ (φ \land x \in (B ∖ ran F)) \to F \cup \{⟨z, x⟩\} \in V$
87		reseq1	$⊢ f = F \cup \{⟨z, x⟩\} \to {f ↾}_{A} = {(F \cup \{⟨z, x⟩\}) ↾}_{A}$
88	87	eqeq1d	$⊢ f = F \cup \{⟨z, x⟩\} \to ({f ↾}_{A} = F \leftrightarrow {(F \cup \{⟨z, x⟩\}) ↾}_{A} = F)$
89		f1eq1	$⊢ f = F \cup \{⟨z, x⟩\} \to (f : A \cup \{z\} \underset{1-1}{⟶} B \leftrightarrow (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} B)$
90	88 89	anbi12d	$⊢ f = F \cup \{⟨z, x⟩\} \to (({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B) \leftrightarrow ({(F \cup \{⟨z, x⟩\}) ↾}_{A} = F \land (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} B))$
91	90	elabg	$⊢ F \cup \{⟨z, x⟩\} \in V \to (F \cup \{⟨z, x⟩\} \in \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \leftrightarrow ({(F \cup \{⟨z, x⟩\}) ↾}_{A} = F \land (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} B))$
92	86 91	syl	$⊢ (φ \land x \in (B ∖ ran F)) \to (F \cup \{⟨z, x⟩\} \in \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \leftrightarrow ({(F \cup \{⟨z, x⟩\}) ↾}_{A} = F \land (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} B))$
93	65 81 92	mpbir2and	$⊢ (φ \land x \in (B ∖ ran F)) \to F \cup \{⟨z, x⟩\} \in \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}$
94	93	ex	$⊢ φ \to (x \in (B ∖ ran F) \to F \cup \{⟨z, x⟩\} \in \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\})$
95	17	anbi1i	$⊢ (g \in \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \land x \in (B ∖ ran F)) \leftrightarrow (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))$
96		simprlr	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to g : A \cup \{z\} \underset{1-1}{⟶} B$
97		f1fn	$⊢ g : A \cup \{z\} \underset{1-1}{⟶} B \to g Fn (A \cup \{z\})$
98	96 97	syl	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to g Fn (A \cup \{z\})$
99	75	adantrl	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1 onto}{⟶} ran F \cup \{x\}$
100		f1ofn	$⊢ (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1 onto}{⟶} ran F \cup \{x\} \to (F \cup \{⟨z, x⟩\}) Fn (A \cup \{z\})$
101	99 100	syl	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to (F \cup \{⟨z, x⟩\}) Fn (A \cup \{z\})$
102		eqfnfv	$⊢ (g Fn (A \cup \{z\}) \land (F \cup \{⟨z, x⟩\}) Fn (A \cup \{z\})) \to (g = F \cup \{⟨z, x⟩\} \leftrightarrow \forall y \in (A \cup \{z\}) g (y) = (F \cup \{⟨z, x⟩\}) (y))$
103	98 101 102	syl2anc	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to (g = F \cup \{⟨z, x⟩\} \leftrightarrow \forall y \in (A \cup \{z\}) g (y) = (F \cup \{⟨z, x⟩\}) (y))$
104		fvres	$⊢ y \in A \to ({g ↾}_{A}) (y) = g (y)$
105	104	eqcomd	$⊢ y \in A \to g (y) = ({g ↾}_{A}) (y)$
106		simprll	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to {g ↾}_{A} = F$
107	106	fveq1d	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to ({g ↾}_{A}) (y) = F (y)$
108	105 107	sylan9eqr	$⊢ ((φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \land y \in A) \to g (y) = F (y)$
109	5	ad2antrr	$⊢ ((φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \land y \in A) \to F : A \underset{1-1}{⟶} B$
110		f1fn	$⊢ F : A \underset{1-1}{⟶} B \to F Fn A$
111	109 110	syl	$⊢ ((φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \land y \in A) \to F Fn A$
112	21 46	fnsn	$⊢ \{⟨z, x⟩\} Fn \{z\}$
113	112	a1i	$⊢ ((φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \land y \in A) \to \{⟨z, x⟩\} Fn \{z\}$
114	59	ad2antrr	$⊢ ((φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \land y \in A) \to A \cap \{z\} = \emptyset$
115		simpr	$⊢ ((φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \land y \in A) \to y \in A$
116	111 113 114 115	fvun1d	$⊢ ((φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \land y \in A) \to (F \cup \{⟨z, x⟩\}) (y) = F (y)$
117	108 116	eqtr4d	$⊢ ((φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \land y \in A) \to g (y) = (F \cup \{⟨z, x⟩\}) (y)$
118	117	ralrimiva	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to \forall y \in A g (y) = (F \cup \{⟨z, x⟩\}) (y)$
119	118	biantrurd	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to (\forall y \in \{z\} g (y) = (F \cup \{⟨z, x⟩\}) (y) \leftrightarrow (\forall y \in A g (y) = (F \cup \{⟨z, x⟩\}) (y) \land \forall y \in \{z\} g (y) = (F \cup \{⟨z, x⟩\}) (y)))$
120		ralunb	$⊢ \forall y \in (A \cup \{z\}) g (y) = (F \cup \{⟨z, x⟩\}) (y) \leftrightarrow (\forall y \in A g (y) = (F \cup \{⟨z, x⟩\}) (y) \land \forall y \in \{z\} g (y) = (F \cup \{⟨z, x⟩\}) (y))$
121	119 120	bitr4di	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to (\forall y \in \{z\} g (y) = (F \cup \{⟨z, x⟩\}) (y) \leftrightarrow \forall y \in (A \cup \{z\}) g (y) = (F \cup \{⟨z, x⟩\}) (y))$
122	44	fdmd	$⊢ φ \to dom F = A$
123	122	eleq2d	$⊢ φ \to (z \in dom F \leftrightarrow z \in A)$
124	3 123	mtbird	$⊢ φ \to \neg z \in dom F$
125	124	adantr	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to \neg z \in dom F$
126		fsnunfv	$⊢ (z \in V \land x \in V \land \neg z \in dom F) \to (F \cup \{⟨z, x⟩\}) (z) = x$
127	21 46 125 126	mp3an12i	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to (F \cup \{⟨z, x⟩\}) (z) = x$
128	127	eqeq2d	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to (g (z) = (F \cup \{⟨z, x⟩\}) (z) \leftrightarrow g (z) = x)$
129		fveq2	$⊢ y = z \to g (y) = g (z)$
130		fveq2	$⊢ y = z \to (F \cup \{⟨z, x⟩\}) (y) = (F \cup \{⟨z, x⟩\}) (z)$
131	129 130	eqeq12d	$⊢ y = z \to (g (y) = (F \cup \{⟨z, x⟩\}) (y) \leftrightarrow g (z) = (F \cup \{⟨z, x⟩\}) (z))$
132	21 131	ralsn	$⊢ \forall y \in \{z\} g (y) = (F \cup \{⟨z, x⟩\}) (y) \leftrightarrow g (z) = (F \cup \{⟨z, x⟩\}) (z)$
133		eqcom	$⊢ x = g (z) \leftrightarrow g (z) = x$
134	128 132 133	3bitr4g	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to (\forall y \in \{z\} g (y) = (F \cup \{⟨z, x⟩\}) (y) \leftrightarrow x = g (z))$
135	103 121 134	3bitr2d	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to (g = F \cup \{⟨z, x⟩\} \leftrightarrow x = g (z))$
136	135	ex	$⊢ φ \to ((({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F)) \to (g = F \cup \{⟨z, x⟩\} \leftrightarrow x = g (z)))$
137	95 136	syl5bi	$⊢ φ \to ((g \in \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \land x \in (B ∖ ran F)) \to (g = F \cup \{⟨z, x⟩\} \leftrightarrow x = g (z)))$
138	10 11 42 94 137	en3d	$⊢ φ \to \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \approx (B ∖ ran F)$

Metamath Proof Explorer

Theorem hashf1lem1

Proof