hashf1lem2

	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\|$
Assertion	hashf1lem2	$⊢ φ \to \|\{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}\| = (\|B\| - \|A\|) \|\{f \| f : A \underset{1-1}{⟶} B\}\|$

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		ssid	$⊢ \{f \| f : A \underset{1-1}{⟶} B\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\}$
6		mapfi	$⊢ (B \in Fin \land A \in Fin) \to B^{A} \in Fin$
7	2 1 6	syl2anc	$⊢ φ \to B^{A} \in Fin$
8		f1f	$⊢ f : A \underset{1-1}{⟶} B \to f : A ⟶ B$
9	2 1	elmapd	$⊢ φ \to (f \in (B^{A}) \leftrightarrow f : A ⟶ B)$
10	8 9	syl5ibr	$⊢ φ \to (f : A \underset{1-1}{⟶} B \to f \in (B^{A}))$
11	10	abssdv	$⊢ φ \to \{f \| f : A \underset{1-1}{⟶} B\} \subseteq B^{A}$
12	7 11	ssfid	$⊢ φ \to \{f \| f : A \underset{1-1}{⟶} B\} \in Fin$
13		sseq1	$⊢ x = \emptyset \to (x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \leftrightarrow \emptyset \subseteq \{f \| f : A \underset{1-1}{⟶} B\})$
14		eleq2	$⊢ x = \emptyset \to ({f ↾}_{A} \in x \leftrightarrow {f ↾}_{A} \in \emptyset)$
15		noel	$⊢ \neg {f ↾}_{A} \in \emptyset$
16	15	pm2.21i	$⊢ {f ↾}_{A} \in \emptyset \to f \in \emptyset$
17	14 16	syl6bi	$⊢ x = \emptyset \to ({f ↾}_{A} \in x \to f \in \emptyset)$
18	17	adantrd	$⊢ x = \emptyset \to (({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B) \to f \in \emptyset)$
19	18	abssdv	$⊢ x = \emptyset \to \{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq \emptyset$
20		ss0	$⊢ \{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq \emptyset \to \{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \emptyset$
21	19 20	syl	$⊢ x = \emptyset \to \{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \emptyset$
22	21	fveq2d	$⊢ x = \emptyset \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\emptyset\|$
23		hash0	$⊢ \|\emptyset\| = 0$
24	22 23	eqtrdi	$⊢ x = \emptyset \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = 0$
25		fveq2	$⊢ x = \emptyset \to \|x\| = \|\emptyset\|$
26	25 23	eqtrdi	$⊢ x = \emptyset \to \|x\| = 0$
27	26	oveq2d	$⊢ x = \emptyset \to (\|B\| - \|A\|) \|x\| = (\|B\| - \|A\|) \cdot 0$
28	24 27	eqeq12d	$⊢ x = \emptyset \to (\|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\| \leftrightarrow 0 = (\|B\| - \|A\|) \cdot 0)$
29	13 28	imbi12d	$⊢ x = \emptyset \to ((x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\|) \leftrightarrow (\emptyset \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to 0 = (\|B\| - \|A\|) \cdot 0))$
30	29	imbi2d	$⊢ x = \emptyset \to ((φ \to (x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\|)) \leftrightarrow (φ \to (\emptyset \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to 0 = (\|B\| - \|A\|) \cdot 0)))$
31		sseq1	$⊢ x = y \to (x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \leftrightarrow y \subseteq \{f \| f : A \underset{1-1}{⟶} B\})$
32		eleq2	$⊢ x = y \to ({f ↾}_{A} \in x \leftrightarrow {f ↾}_{A} \in y)$
33	32	anbi1d	$⊢ x = y \to (({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B) \leftrightarrow ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B))$
34	33	abbidv	$⊢ x = y \to \{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}$
35	34	fveq2d	$⊢ x = y \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\|$
36		fveq2	$⊢ x = y \to \|x\| = \|y\|$
37	36	oveq2d	$⊢ x = y \to (\|B\| - \|A\|) \|x\| = (\|B\| - \|A\|) \|y\|$
38	35 37	eqeq12d	$⊢ x = y \to (\|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\| \leftrightarrow \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\|)$
39	31 38	imbi12d	$⊢ x = y \to ((x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\|) \leftrightarrow (y \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\|))$
40	39	imbi2d	$⊢ x = y \to ((φ \to (x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\|)) \leftrightarrow (φ \to (y \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\|)))$
41		sseq1	$⊢ x = y \cup \{a\} \to (x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \leftrightarrow y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})$
42		eleq2	$⊢ x = y \cup \{a\} \to ({f ↾}_{A} \in x \leftrightarrow {f ↾}_{A} \in (y \cup \{a\}))$
43	42	anbi1d	$⊢ x = y \cup \{a\} \to (({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B) \leftrightarrow ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B))$
44	43	abbidv	$⊢ x = y \cup \{a\} \to \{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}$
45	44	fveq2d	$⊢ x = y \cup \{a\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\|$
46		fveq2	$⊢ x = y \cup \{a\} \to \|x\| = \|y \cup \{a\}\|$
47	46	oveq2d	$⊢ x = y \cup \{a\} \to (\|B\| - \|A\|) \|x\| = (\|B\| - \|A\|) \|y \cup \{a\}\|$
48	45 47	eqeq12d	$⊢ x = y \cup \{a\} \to (\|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\| \leftrightarrow \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\|)$
49	41 48	imbi12d	$⊢ x = y \cup \{a\} \to ((x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\|) \leftrightarrow (y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\|))$
50	49	imbi2d	$⊢ x = y \cup \{a\} \to ((φ \to (x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\|)) \leftrightarrow (φ \to (y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\|)))$
51		sseq1	$⊢ x = \{f \| f : A \underset{1-1}{⟶} B\} \to (x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \leftrightarrow \{f \| f : A \underset{1-1}{⟶} B\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})$
52		f1eq1	$⊢ f = y \to (f : A \underset{1-1}{⟶} B \leftrightarrow y : A \underset{1-1}{⟶} B)$
53	52	cbvabv	$⊢ \{f \| f : A \underset{1-1}{⟶} B\} = \{y \| y : A \underset{1-1}{⟶} B\}$
54	53	eqeq2i	$⊢ x = \{f \| f : A \underset{1-1}{⟶} B\} \leftrightarrow x = \{y \| y : A \underset{1-1}{⟶} B\}$
55		ssun1	$⊢ A \subseteq A \cup \{z\}$
56		f1ssres	$⊢ (f : A \cup \{z\} \underset{1-1}{⟶} B \land A \subseteq A \cup \{z\}) \to ({f ↾}_{A}) : A \underset{1-1}{⟶} B$
57	55 56	mpan2	$⊢ f : A \cup \{z\} \underset{1-1}{⟶} B \to ({f ↾}_{A}) : A \underset{1-1}{⟶} B$
58		vex	$⊢ f \in V$
59	58	resex	$⊢ {f ↾}_{A} \in V$
60		f1eq1	$⊢ y = {f ↾}_{A} \to (y : A \underset{1-1}{⟶} B \leftrightarrow ({f ↾}_{A}) : A \underset{1-1}{⟶} B)$
61	59 60	elab	$⊢ {f ↾}_{A} \in \{y \| y : A \underset{1-1}{⟶} B\} \leftrightarrow ({f ↾}_{A}) : A \underset{1-1}{⟶} B$
62	57 61	sylibr	$⊢ f : A \cup \{z\} \underset{1-1}{⟶} B \to {f ↾}_{A} \in \{y \| y : A \underset{1-1}{⟶} B\}$
63		eleq2	$⊢ x = \{y \| y : A \underset{1-1}{⟶} B\} \to ({f ↾}_{A} \in x \leftrightarrow {f ↾}_{A} \in \{y \| y : A \underset{1-1}{⟶} B\})$
64	62 63	syl5ibr	$⊢ x = \{y \| y : A \underset{1-1}{⟶} B\} \to (f : A \cup \{z\} \underset{1-1}{⟶} B \to {f ↾}_{A} \in x)$
65	64	pm4.71rd	$⊢ x = \{y \| y : A \underset{1-1}{⟶} B\} \to (f : A \cup \{z\} \underset{1-1}{⟶} B \leftrightarrow ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B))$
66	65	bicomd	$⊢ x = \{y \| y : A \underset{1-1}{⟶} B\} \to (({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B) \leftrightarrow f : A \cup \{z\} \underset{1-1}{⟶} B)$
67	66	abbidv	$⊢ x = \{y \| y : A \underset{1-1}{⟶} B\} \to \{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}$
68	54 67	sylbi	$⊢ x = \{f \| f : A \underset{1-1}{⟶} B\} \to \{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}$
69	68	fveq2d	$⊢ x = \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}\|$
70		fveq2	$⊢ x = \{f \| f : A \underset{1-1}{⟶} B\} \to \|x\| = \|\{f \| f : A \underset{1-1}{⟶} B\}\|$
71	70	oveq2d	$⊢ x = \{f \| f : A \underset{1-1}{⟶} B\} \to (\|B\| - \|A\|) \|x\| = (\|B\| - \|A\|) \|\{f \| f : A \underset{1-1}{⟶} B\}\|$
72	69 71	eqeq12d	$⊢ x = \{f \| f : A \underset{1-1}{⟶} B\} \to (\|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\| \leftrightarrow \|\{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}\| = (\|B\| - \|A\|) \|\{f \| f : A \underset{1-1}{⟶} B\}\|)$
73	51 72	imbi12d	$⊢ x = \{f \| f : A \underset{1-1}{⟶} B\} \to ((x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\|) \leftrightarrow (\{f \| f : A \underset{1-1}{⟶} B\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}\| = (\|B\| - \|A\|) \|\{f \| f : A \underset{1-1}{⟶} B\}\|))$
74	73	imbi2d	$⊢ x = \{f \| f : A \underset{1-1}{⟶} B\} \to ((φ \to (x \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in x \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|x\|)) \leftrightarrow (φ \to (\{f \| f : A \underset{1-1}{⟶} B\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}\| = (\|B\| - \|A\|) \|\{f \| f : A \underset{1-1}{⟶} B\}\|)))$
75		hashcl	$⊢ B \in Fin \to \|B\| \in ℕ_{0}$
76	2 75	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
77	76	nn0cnd	$⊢ φ \to \|B\| \in ℂ$
78		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
79	1 78	syl	$⊢ φ \to \|A\| \in ℕ_{0}$
80	79	nn0cnd	$⊢ φ \to \|A\| \in ℂ$
81	77 80	subcld	$⊢ φ \to \|B\| - \|A\| \in ℂ$
82	81	mul01d	$⊢ φ \to (\|B\| - \|A\|) \cdot 0 = 0$
83	82	eqcomd	$⊢ φ \to 0 = (\|B\| - \|A\|) \cdot 0$
84	83	a1d	$⊢ φ \to (\emptyset \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to 0 = (\|B\| - \|A\|) \cdot 0)$
85		ssun1	$⊢ y \subseteq y \cup \{a\}$
86		sstr	$⊢ (y \subseteq y \cup \{a\} \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\}) \to y \subseteq \{f \| f : A \underset{1-1}{⟶} B\}$
87	85 86	mpan	$⊢ y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to y \subseteq \{f \| f : A \underset{1-1}{⟶} B\}$
88	87	imim1i	$⊢ (y \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\|) \to (y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\|)$
89		oveq1	$⊢ \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\| \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| + \|B\| - \|A\| = (\|B\| - \|A\|) \|y\| + \|B\| - \|A\|$
90		elun	$⊢ {f ↾}_{A} \in (y \cup \{a\}) \leftrightarrow ({f ↾}_{A} \in y \lor {f ↾}_{A} \in \{a\})$
91	59	elsn	$⊢ {f ↾}_{A} \in \{a\} \leftrightarrow {f ↾}_{A} = a$
92	91	orbi2i	$⊢ ({f ↾}_{A} \in y \lor {f ↾}_{A} \in \{a\}) \leftrightarrow ({f ↾}_{A} \in y \lor {f ↾}_{A} = a)$
93	90 92	bitri	$⊢ {f ↾}_{A} \in (y \cup \{a\}) \leftrightarrow ({f ↾}_{A} \in y \lor {f ↾}_{A} = a)$
94	93	anbi1i	$⊢ ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B) \leftrightarrow (({f ↾}_{A} \in y \lor {f ↾}_{A} = a) \land f : A \cup \{z\} \underset{1-1}{⟶} B)$
95		andir	$⊢ (({f ↾}_{A} \in y \lor {f ↾}_{A} = a) \land f : A \cup \{z\} \underset{1-1}{⟶} B) \leftrightarrow (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \lor ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))$
96	94 95	bitri	$⊢ ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B) \leftrightarrow (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \lor ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))$
97	96	abbii	$⊢ \{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \{f \| (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \lor ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))\}$
98		unab	$⊢ \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \cup \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \{f \| (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \lor ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))\}$
99	97 98	eqtr4i	$⊢ \{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \cup \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}$
100	99	fveq2i	$⊢ \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \cup \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\|$
101		snfi	$⊢ \{z\} \in Fin$
102		unfi	$⊢ (A \in Fin \land \{z\} \in Fin) \to A \cup \{z\} \in Fin$
103	1 101 102	sylancl	$⊢ φ \to A \cup \{z\} \in Fin$
104		mapvalg	$⊢ (B \in Fin \land A \cup \{z\} \in Fin) \to B^{(A \cup \{z\})} = \{f \| f : A \cup \{z\} ⟶ B\}$
105	2 103 104	syl2anc	$⊢ φ \to B^{(A \cup \{z\})} = \{f \| f : A \cup \{z\} ⟶ B\}$
106		mapfi	$⊢ (B \in Fin \land A \cup \{z\} \in Fin) \to B^{(A \cup \{z\})} \in Fin$
107	2 103 106	syl2anc	$⊢ φ \to B^{(A \cup \{z\})} \in Fin$
108	105 107	eqeltrrd	$⊢ φ \to \{f \| f : A \cup \{z\} ⟶ B\} \in Fin$
109		f1f	$⊢ f : A \cup \{z\} \underset{1-1}{⟶} B \to f : A \cup \{z\} ⟶ B$
110	109	adantl	$⊢ ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \to f : A \cup \{z\} ⟶ B$
111	110	ss2abi	$⊢ \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq \{f \| f : A \cup \{z\} ⟶ B\}$
112		ssfi	$⊢ (\{f \| f : A \cup \{z\} ⟶ B\} \in Fin \land \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq \{f \| f : A \cup \{z\} ⟶ B\}) \to \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin$
113	108 111 112	sylancl	$⊢ φ \to \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin$
114	113	adantr	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin$
115	109	adantl	$⊢ ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B) \to f : A \cup \{z\} ⟶ B$
116	115	ss2abi	$⊢ \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq \{f \| f : A \cup \{z\} ⟶ B\}$
117		ssfi	$⊢ (\{f \| f : A \cup \{z\} ⟶ B\} \in Fin \land \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \subseteq \{f \| f : A \cup \{z\} ⟶ B\}) \to \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin$
118	108 116 117	sylancl	$⊢ φ \to \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin$
119	118	adantr	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin$
120		inab	$⊢ \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \cap \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \{f \| (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))\}$
121		simprlr	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \neg a \in y$
122		abn0	$⊢ \{f \| (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))\} \neq \emptyset \leftrightarrow \exists f (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))$
123		simprl	$⊢ (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)) \to {f ↾}_{A} = a$
124		simpll	$⊢ (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)) \to {f ↾}_{A} \in y$
125	123 124	eqeltrrd	$⊢ (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)) \to a \in y$
126	125	exlimiv	$⊢ \exists f (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)) \to a \in y$
127	122 126	sylbi	$⊢ \{f \| (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))\} \neq \emptyset \to a \in y$
128	127	necon1bi	$⊢ \neg a \in y \to \{f \| (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))\} = \emptyset$
129	121 128	syl	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \{f \| (({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B) \land ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B))\} = \emptyset$
130	120 129	syl5eq	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \cap \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \emptyset$
131		hashun	$⊢ (\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin \land \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin \land \{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \cap \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} = \emptyset) \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \cup \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| + \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\|$
132	114 119 130 131	syl3anc	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \cup \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| + \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\|$
133	100 132	syl5eq	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| + \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\|$
134		simpr	$⊢ ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\}) \to y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\}$
135	134	unssbd	$⊢ ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\}) \to \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\}$
136		vex	$⊢ a \in V$
137	136	snss	$⊢ a \in \{f \| f : A \underset{1-1}{⟶} B\} \leftrightarrow \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\}$
138	135 137	sylibr	$⊢ ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\}) \to a \in \{f \| f : A \underset{1-1}{⟶} B\}$
139		f1eq1	$⊢ f = a \to (f : A \underset{1-1}{⟶} B \leftrightarrow a : A \underset{1-1}{⟶} B)$
140	136 139	elab	$⊢ a \in \{f \| f : A \underset{1-1}{⟶} B\} \leftrightarrow a : A \underset{1-1}{⟶} B$
141	138 140	sylib	$⊢ ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\}) \to a : A \underset{1-1}{⟶} B$
142	80	adantr	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|A\| \in ℂ$
143	118	adantr	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin$
144		hashcl	$⊢ \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \in Fin \to \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| \in ℕ_{0}$
145	143 144	syl	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| \in ℕ_{0}$
146	145	nn0cnd	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| \in ℂ$
147	142 146	pncan2d	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|A\| + \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| - \|A\| = \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\|$
148		f1f1orn	$⊢ a : A \underset{1-1}{⟶} B \to a : A \underset{1-1 onto}{⟶} ran a$
149	148	adantl	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to a : A \underset{1-1 onto}{⟶} ran a$
150		f1oen3g	$⊢ (a \in V \land a : A \underset{1-1 onto}{⟶} ran a) \to A \approx ran a$
151	136 149 150	sylancr	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to A \approx ran a$
152		hasheni	$⊢ A \approx ran a \to \|A\| = \|ran a\|$
153	151 152	syl	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|A\| = \|ran a\|$
154	1	adantr	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to A \in Fin$
155	2	adantr	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to B \in Fin$
156	3	adantr	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \neg z \in A$
157	4	adantr	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|A\| + 1 \leq \|B\|$
158		simpr	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to a : A \underset{1-1}{⟶} B$
159	154 155 156 157 158	hashf1lem1	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \approx (B ∖ ran a)$
160		hasheni	$⊢ \{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\} \approx (B ∖ ran a) \to \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|B ∖ ran a\|$
161	159 160	syl	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|B ∖ ran a\|$
162	153 161	oveq12d	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|A\| + \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|ran a\| + \|B ∖ ran a\|$
163		f1f	$⊢ a : A \underset{1-1}{⟶} B \to a : A ⟶ B$
164	163	frnd	$⊢ a : A \underset{1-1}{⟶} B \to ran a \subseteq B$
165	164	adantl	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to ran a \subseteq B$
166	155 165	ssfid	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to ran a \in Fin$
167		diffi	$⊢ B \in Fin \to B ∖ ran a \in Fin$
168	155 167	syl	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to B ∖ ran a \in Fin$
169		disjdif	$⊢ ran a \cap (B ∖ ran a) = \emptyset$
170	169	a1i	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to ran a \cap (B ∖ ran a) = \emptyset$
171		hashun	$⊢ (ran a \in Fin \land B ∖ ran a \in Fin \land ran a \cap (B ∖ ran a) = \emptyset) \to \|ran a \cup (B ∖ ran a)\| = \|ran a\| + \|B ∖ ran a\|$
172	166 168 170 171	syl3anc	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|ran a \cup (B ∖ ran a)\| = \|ran a\| + \|B ∖ ran a\|$
173		undif	$⊢ ran a \subseteq B \leftrightarrow ran a \cup (B ∖ ran a) = B$
174	165 173	sylib	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to ran a \cup (B ∖ ran a) = B$
175	174	fveq2d	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|ran a \cup (B ∖ ran a)\| = \|B\|$
176	162 172 175	3eqtr2d	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|A\| + \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|B\|$
177	176	oveq1d	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|A\| + \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| - \|A\| = \|B\| - \|A\|$
178	147 177	eqtr3d	$⊢ (φ \land a : A \underset{1-1}{⟶} B) \to \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|B\| - \|A\|$
179	141 178	sylan2	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|B\| - \|A\|$
180	179	oveq2d	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| + \|\{f \| ({f ↾}_{A} = a \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| + \|B\| - \|A\|$
181	133 180	eqtrd	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| + \|B\| - \|A\|$
182		hashunsng	$⊢ a \in V \to ((y \in Fin \land \neg a \in y) \to \|y \cup \{a\}\| = \|y\| + 1)$
183	182	elv	$⊢ (y \in Fin \land \neg a \in y) \to \|y \cup \{a\}\| = \|y\| + 1$
184	183	ad2antrl	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \|y \cup \{a\}\| = \|y\| + 1$
185	184	oveq2d	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to (\|B\| - \|A\|) \|y \cup \{a\}\| = (\|B\| - \|A\|) (\|y\| + 1)$
186	81	adantr	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \|B\| - \|A\| \in ℂ$
187		simprll	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to y \in Fin$
188		hashcl	$⊢ y \in Fin \to \|y\| \in ℕ_{0}$
189	187 188	syl	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \|y\| \in ℕ_{0}$
190	189	nn0cnd	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to \|y\| \in ℂ$
191		1cnd	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to 1 \in ℂ$
192	186 190 191	adddid	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to (\|B\| - \|A\|) (\|y\| + 1) = (\|B\| - \|A\|) \|y\| + (\|B\| - \|A\|) \cdot 1$
193	186	mulid1d	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to (\|B\| - \|A\|) \cdot 1 = \|B\| - \|A\|$
194	193	oveq2d	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to (\|B\| - \|A\|) \|y\| + (\|B\| - \|A\|) \cdot 1 = (\|B\| - \|A\|) \|y\| + \|B\| - \|A\|$
195	185 192 194	3eqtrd	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to (\|B\| - \|A\|) \|y \cup \{a\}\| = (\|B\| - \|A\|) \|y\| + \|B\| - \|A\|$
196	181 195	eqeq12d	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to (\|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\| \leftrightarrow \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| + \|B\| - \|A\| = (\|B\| - \|A\|) \|y\| + \|B\| - \|A\|)$
197	89 196	syl5ibr	$⊢ (φ \land ((y \in Fin \land \neg a \in y) \land y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\})) \to (\|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\| \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\|)$
198	197	expr	$⊢ (φ \land (y \in Fin \land \neg a \in y)) \to (y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to (\|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\| \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\|))$
199	198	a2d	$⊢ (φ \land (y \in Fin \land \neg a \in y)) \to ((y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\|) \to (y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\|))$
200	88 199	syl5	$⊢ (φ \land (y \in Fin \land \neg a \in y)) \to ((y \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\|) \to (y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\|))$
201	200	expcom	$⊢ (y \in Fin \land \neg a \in y) \to (φ \to ((y \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\|) \to (y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\|)))$
202	201	a2d	$⊢ (y \in Fin \land \neg a \in y) \to ((φ \to (y \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in y \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y\|)) \to (φ \to (y \cup \{a\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| ({f ↾}_{A} \in (y \cup \{a\}) \land f : A \cup \{z\} \underset{1-1}{⟶} B)\}\| = (\|B\| - \|A\|) \|y \cup \{a\}\|)))$
203	30 40 50 74 84 202	findcard2s	$⊢ \{f \| f : A \underset{1-1}{⟶} B\} \in Fin \to (φ \to (\{f \| f : A \underset{1-1}{⟶} B\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}\| = (\|B\| - \|A\|) \|\{f \| f : A \underset{1-1}{⟶} B\}\|))$
204	12 203	mpcom	$⊢ φ \to (\{f \| f : A \underset{1-1}{⟶} B\} \subseteq \{f \| f : A \underset{1-1}{⟶} B\} \to \|\{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}\| = (\|B\| - \|A\|) \|\{f \| f : A \underset{1-1}{⟶} B\}\|)$
205	5 204	mpi	$⊢ φ \to \|\{f \| f : A \cup \{z\} \underset{1-1}{⟶} B\}\| = (\|B\| - \|A\|) \|\{f \| f : A \underset{1-1}{⟶} B\}\|$

Metamath Proof Explorer

Theorem hashf1lem2

Proof