hashf1lem1OLD

Description: Obsolete version of hashf1lem1 as of 7-Aug-2024. (Contributed by Mario Carneiro, 17-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	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	hashf1lem1OLD	$⊢ φ \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		f1f	$⊢ f : A \cup \{z\} \underset{1-1}{⟶} B \to f : A \cup \{z\} ⟶ B$
7	6	adantl	$⊢ ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B) \to f : A \cup \{z\} ⟶ B$
8		snfi	$⊢ \{z\} \in Fin$
9		unfi	$⊢ (A \in Fin \land \{z\} \in Fin) \to A \cup \{z\} \in Fin$
10	1 8 9	sylancl	$⊢ φ \to A \cup \{z\} \in Fin$
11	2 10	elmapd	$⊢ φ \to (f \in (B^{(A \cup \{z\})}) \leftrightarrow f : A \cup \{z\} ⟶ B)$
12	7 11	syl5ibr	$⊢ φ \to (({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B) \to f \in (B^{(A \cup \{z\})}))$
13	12	abssdv	$⊢ φ \to \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq B^{(A \cup \{z\})}$
14		ovex	$⊢ B^{(A \cup \{z\})} \in V$
15		ssexg	$⊢ (\{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq B^{(A \cup \{z\})} \land B^{(A \cup \{z\})} \in V) \to \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in V$
16	13 14 15	sylancl	$⊢ φ \to \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in V$
17		difexg	$⊢ B \in Fin \to B ∖ ran F \in V$
18	2 17	syl	$⊢ φ \to B ∖ ran F \in V$
19		vex	$⊢ g \in V$
20		reseq1	$⊢ f = g \to {f ↾}_{A} = {g ↾}_{A}$
21	20	eqeq1d	$⊢ f = g \to ({f ↾}_{A} = F \leftrightarrow {g ↾}_{A} = F)$
22		f1eq1	$⊢ f = g \to (f : A \cup \{z\} \underset{1-1}{⟶} B \leftrightarrow g : A \cup \{z\} \underset{1-1}{⟶} B)$
23	21 22	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))$
24	19 23	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)$
25		f1f	$⊢ g : A \cup \{z\} \underset{1-1}{⟶} B \to g : A \cup \{z\} ⟶ B$
26	25	ad2antll	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g : A \cup \{z\} ⟶ B$
27		ssun2	$⊢ \{z\} \subseteq A \cup \{z\}$
28		vex	$⊢ z \in V$
29	28	snss	$⊢ z \in (A \cup \{z\}) \leftrightarrow \{z\} \subseteq A \cup \{z\}$
30	27 29	mpbir	$⊢ z \in (A \cup \{z\})$
31		ffvelrn	$⊢ (g : A \cup \{z\} ⟶ B \land z \in (A \cup \{z\})) \to g (z) \in B$
32	26 30 31	sylancl	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g (z) \in B$
33	3	adantr	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to \neg z \in A$
34		df-ima	$⊢ g [A] = ran ({g ↾}_{A})$
35		simprl	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to {g ↾}_{A} = F$
36	35	rneqd	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to ran ({g ↾}_{A}) = ran F$
37	34 36	eqtrid	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g [A] = ran F$
38	37	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)$
39		simprr	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g : A \cup \{z\} \underset{1-1}{⟶} B$
40	30	a1i	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to z \in (A \cup \{z\})$
41		ssun1	$⊢ A \subseteq A \cup \{z\}$
42	41	a1i	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to A \subseteq A \cup \{z\}$
43		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)$
44	39 40 42 43	syl3anc	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to (g (z) \in g [A] \leftrightarrow z \in A)$
45	38 44	bitr3d	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to (g (z) \in ran F \leftrightarrow z \in A)$
46	33 45	mtbird	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to \neg g (z) \in ran F$
47	32 46	eldifd	$⊢ (φ \land ({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B)) \to g (z) \in (B ∖ ran F)$
48	47	ex	$⊢ φ \to (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \to g (z) \in (B ∖ ran F))$
49	24 48	syl5bi	$⊢ φ \to (g \in \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \to g (z) \in (B ∖ ran F))$
50		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
51	5 50	syl	$⊢ φ \to F : A ⟶ B$
52	51	adantr	$⊢ (φ \land x \in (B ∖ ran F)) \to F : A ⟶ B$
53		vex	$⊢ x \in V$
54	28 53	f1osn	$⊢ \{⟨z, x⟩\} : \{z\} \underset{1-1 onto}{⟶} \{x\}$
55		f1of	$⊢ \{⟨z, x⟩\} : \{z\} \underset{1-1 onto}{⟶} \{x\} \to \{⟨z, x⟩\} : \{z\} ⟶ \{x\}$
56	54 55	ax-mp	$⊢ \{⟨z, x⟩\} : \{z\} ⟶ \{x\}$
57		eldifi	$⊢ x \in (B ∖ ran F) \to x \in B$
58	57	adantl	$⊢ (φ \land x \in (B ∖ ran F)) \to x \in B$
59	58	snssd	$⊢ (φ \land x \in (B ∖ ran F)) \to \{x\} \subseteq B$
60		fss	$⊢ (\{⟨z, x⟩\} : \{z\} ⟶ \{x\} \land \{x\} \subseteq B) \to \{⟨z, x⟩\} : \{z\} ⟶ B$
61	56 59 60	sylancr	$⊢ (φ \land x \in (B ∖ ran F)) \to \{⟨z, x⟩\} : \{z\} ⟶ B$
62		res0	$⊢ {F ↾}_{\emptyset} = \emptyset$
63		res0	$⊢ {\{⟨z, x⟩\} ↾}_{\emptyset} = \emptyset$
64	62 63	eqtr4i	$⊢ {F ↾}_{\emptyset} = {\{⟨z, x⟩\} ↾}_{\emptyset}$
65		disjsn	$⊢ A \cap \{z\} = \emptyset \leftrightarrow \neg z \in A$
66	3 65	sylibr	$⊢ φ \to A \cap \{z\} = \emptyset$
67	66	adantr	$⊢ (φ \land x \in (B ∖ ran F)) \to A \cap \{z\} = \emptyset$
68	67	reseq2d	$⊢ (φ \land x \in (B ∖ ran F)) \to {F ↾}_{(A \cap \{z\})} = {F ↾}_{\emptyset}$
69	67	reseq2d	$⊢ (φ \land x \in (B ∖ ran F)) \to {\{⟨z, x⟩\} ↾}_{(A \cap \{z\})} = {\{⟨z, x⟩\} ↾}_{\emptyset}$
70	64 68 69	3eqtr4a	$⊢ (φ \land x \in (B ∖ ran F)) \to {F ↾}_{(A \cap \{z\})} = {\{⟨z, x⟩\} ↾}_{(A \cap \{z\})}$
71		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$
72	52 61 70 71	syl3anc	$⊢ (φ \land x \in (B ∖ ran F)) \to {(F \cup \{⟨z, x⟩\}) ↾}_{A} = F$
73		f1f1orn	$⊢ F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} ran F$
74	5 73	syl	$⊢ φ \to F : A \underset{1-1 onto}{⟶} ran F$
75	74	adantr	$⊢ (φ \land x \in (B ∖ ran F)) \to F : A \underset{1-1 onto}{⟶} ran F$
76	54	a1i	$⊢ (φ \land x \in (B ∖ ran F)) \to \{⟨z, x⟩\} : \{z\} \underset{1-1 onto}{⟶} \{x\}$
77		eldifn	$⊢ x \in (B ∖ ran F) \to \neg x \in ran F$
78	77	adantl	$⊢ (φ \land x \in (B ∖ ran F)) \to \neg x \in ran F$
79		disjsn	$⊢ ran F \cap \{x\} = \emptyset \leftrightarrow \neg x \in ran F$
80	78 79	sylibr	$⊢ (φ \land x \in (B ∖ ran F)) \to ran F \cap \{x\} = \emptyset$
81		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\}$
82	75 76 67 80 81	syl22anc	$⊢ (φ \land x \in (B ∖ ran F)) \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1 onto}{⟶} ran F \cup \{x\}$
83		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\}$
84	82 83	syl	$⊢ (φ \land x \in (B ∖ ran F)) \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} ran F \cup \{x\}$
85	52	frnd	$⊢ (φ \land x \in (B ∖ ran F)) \to ran F \subseteq B$
86	85 59	unssd	$⊢ (φ \land x \in (B ∖ ran F)) \to ran F \cup \{x\} \subseteq B$
87		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$
88	84 86 87	syl2anc	$⊢ (φ \land x \in (B ∖ ran F)) \to (F \cup \{⟨z, x⟩\}) : A \cup \{z\} \underset{1-1}{⟶} B$
89	51 1	fexd	$⊢ φ \to F \in V$
90	89	adantr	$⊢ (φ \land x \in (B ∖ ran F)) \to F \in V$
91		snex	$⊢ \{⟨z, x⟩\} \in V$
92		unexg	$⊢ (F \in V \land \{⟨z, x⟩\} \in V) \to F \cup \{⟨z, x⟩\} \in V$
93	90 91 92	sylancl	$⊢ (φ \land x \in (B ∖ ran F)) \to F \cup \{⟨z, x⟩\} \in V$
94		reseq1	$⊢ f = F \cup \{⟨z, x⟩\} \to {f ↾}_{A} = {(F \cup \{⟨z, x⟩\}) ↾}_{A}$
95	94	eqeq1d	$⊢ f = F \cup \{⟨z, x⟩\} \to ({f ↾}_{A} = F \leftrightarrow {(F \cup \{⟨z, x⟩\}) ↾}_{A} = F)$
96		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)$
97	95 96	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))$
98	97	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))$
99	93 98	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))$
100	72 88 99	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)\}$
101	100	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)\})$
102	24	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))$
103		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$
104		f1fn	$⊢ g : A \cup \{z\} \underset{1-1}{⟶} B \to g Fn (A \cup \{z\})$
105	103 104	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\})$
106	82	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\}$
107		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\})$
108	106 107	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\})$
109		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))$
110	105 108 109	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))$
111		fvres	$⊢ y \in A \to ({g ↾}_{A}) (y) = g (y)$
112	111	eqcomd	$⊢ y \in A \to g (y) = ({g ↾}_{A}) (y)$
113		simprll	$⊢ (φ \land (({g ↾}_{A} = F \land g : A \cup \{z\} \underset{1-1}{⟶} B) \land x \in (B ∖ ran F))) \to {g ↾}_{A} = F$
114	113	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)$
115	112 114	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)$
116	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$
117		f1fn	$⊢ F : A \underset{1-1}{⟶} B \to F Fn A$
118	116 117	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$
119	28 53	fnsn	$⊢ \{⟨z, x⟩\} Fn \{z\}$
120	119	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\}$
121	66	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$
122		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$
123	118 120 121 122	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)$
124	115 123	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)$
125	124	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)$
126	125	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)))$
127		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))$
128	126 127	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))$
129	51	fdmd	$⊢ φ \to dom F = A$
130	129	eleq2d	$⊢ φ \to (z \in dom F \leftrightarrow z \in A)$
131	3 130	mtbird	$⊢ φ \to \neg z \in dom F$
132	131	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$
133		fsnunfv	$⊢ (z \in V \land x \in V \land \neg z \in dom F) \to (F \cup \{⟨z, x⟩\}) (z) = x$
134	28 53 132 133	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$
135	134	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)$
136		fveq2	$⊢ y = z \to g (y) = g (z)$
137		fveq2	$⊢ y = z \to (F \cup \{⟨z, x⟩\}) (y) = (F \cup \{⟨z, x⟩\}) (z)$
138	136 137	eqeq12d	$⊢ y = z \to (g (y) = (F \cup \{⟨z, x⟩\}) (y) \leftrightarrow g (z) = (F \cup \{⟨z, x⟩\}) (z))$
139	28 138	ralsn	$⊢ \forall y \in \{z\} g (y) = (F \cup \{⟨z, x⟩\}) (y) \leftrightarrow g (z) = (F \cup \{⟨z, x⟩\}) (z)$
140		eqcom	$⊢ x = g (z) \leftrightarrow g (z) = x$
141	135 139 140	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))$
142	110 128 141	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))$
143	142	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)))$
144	102 143	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)))$
145	16 18 49 101 144	en3d	$⊢ φ \to \{f \| ({f ↾}_{A} = F \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \approx (B ∖ ran F)$

Metamath Proof Explorer

Theorem hashf1lem1OLD

Proof