hashf1lem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hashf1lem2		Structured version Visualization version GIF version

Theorem hashf1lem2 13240

Description: Lemma for hashf1 13241. (Contributed by Mario Carneiro, 17-Apr-2015.)

**Hypotheses**
Ref	Expression
hashf1lem2.1	⊢ (𝜑 → 𝐴 ∈ Fin)
hashf1lem2.2	⊢ (𝜑 → 𝐵 ∈ Fin)
hashf1lem2.3	⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)
hashf1lem2.4	⊢ (𝜑 → ((#‘𝐴) + 1) ≤ (#‘𝐵))

**Assertion**
Ref	Expression
hashf1lem2	⊢ (𝜑 → (#‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})))

Distinct variable groups: 𝑧,𝑓 𝐴,𝑓 𝐵,𝑓 𝜑,𝑓 Allowed substitution hints: 𝜑(𝑧) 𝐴(𝑧) 𝐵(𝑧)

Proof of Theorem hashf1lem2 Dummy variables 𝑎 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssid 3624	. 2 ⊢ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}
2		hashf1lem2.2	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ Fin)
3		hashf1lem2.1	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ Fin)
4		mapfi 8262	. . . . 5 ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ∈ Fin) → (𝐵 ↑_𝑚 𝐴) ∈ Fin)
5	2, 3, 4	syl2anc 693	. . . 4 ⊢ (𝜑 → (𝐵 ↑_𝑚 𝐴) ∈ Fin)
6		f1f 6101	. . . . . 6 ⊢ (𝑓:𝐴–1-1→𝐵 → 𝑓:𝐴⟶𝐵)
7	2, 3	elmapd 7871	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑_𝑚 𝐴) ↔ 𝑓:𝐴⟶𝐵))
8	6, 7	syl5ibr 236	. . . . 5 ⊢ (𝜑 → (𝑓:𝐴–1-1→𝐵 → 𝑓 ∈ (𝐵 ↑_𝑚 𝐴)))
9	8	abssdv 3676	. . . 4 ⊢ (𝜑 → {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ⊆ (𝐵 ↑_𝑚 𝐴))
10		ssfi 8180	. . . 4 ⊢ (((𝐵 ↑_𝑚 𝐴) ∈ Fin ∧ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ⊆ (𝐵 ↑_𝑚 𝐴)) → {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ∈ Fin)
11	5, 9, 10	syl2anc 693	. . 3 ⊢ (𝜑 → {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ∈ Fin)
12		sseq1 3626	. . . . . 6 ⊢ (𝑥 = ∅ → (𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ↔ ∅ ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))
13		eleq2 2690	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → ((𝑓 ↾ 𝐴) ∈ 𝑥 ↔ (𝑓 ↾ 𝐴) ∈ ∅))
14		noel 3919	. . . . . . . . . . . . . 14 ⊢ ¬ (𝑓 ↾ 𝐴) ∈ ∅
15	14	pm2.21i 116	. . . . . . . . . . . . 13 ⊢ ((𝑓 ↾ 𝐴) ∈ ∅ → 𝑓 ∈ ∅)
16	13, 15	syl6bi 243	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → ((𝑓 ↾ 𝐴) ∈ 𝑥 → 𝑓 ∈ ∅))
17	16	adantrd 484	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) → 𝑓 ∈ ∅))
18	17	abssdv 3676	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ ∅)
19		ss0 3974	. . . . . . . . . 10 ⊢ ({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ ∅ → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} = ∅)
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (𝑥 = ∅ → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} = ∅)
21	20	fveq2d 6195	. . . . . . . 8 ⊢ (𝑥 = ∅ → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (#‘∅))
22		hash0 13158	. . . . . . . 8 ⊢ (#‘∅) = 0
23	21, 22	syl6eq 2672	. . . . . . 7 ⊢ (𝑥 = ∅ → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = 0)
24		fveq2 6191	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (#‘𝑥) = (#‘∅))
25	24, 22	syl6eq 2672	. . . . . . . 8 ⊢ (𝑥 = ∅ → (#‘𝑥) = 0)
26	25	oveq2d 6666	. . . . . . 7 ⊢ (𝑥 = ∅ → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · 0))
27	23, 26	eqeq12d 2637	. . . . . 6 ⊢ (𝑥 = ∅ → ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ 0 = (((#‘𝐵) − (#‘𝐴)) · 0)))
28	12, 27	imbi12d 334	. . . . 5 ⊢ (𝑥 = ∅ → ((𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ (∅ ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → 0 = (((#‘𝐵) − (#‘𝐴)) · 0))))
29	28	imbi2d 330	. . . 4 ⊢ (𝑥 = ∅ → ((𝜑 → (𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → (∅ ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → 0 = (((#‘𝐵) − (#‘𝐴)) · 0)))))
30		sseq1 3626	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ↔ 𝑦 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))
31		eleq2 2690	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑓 ↾ 𝐴) ∈ 𝑥 ↔ (𝑓 ↾ 𝐴) ∈ 𝑦))
32	31	anbi1d 741	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)))
33	32	abbidv 2741	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} = {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})
34	33	fveq2d 6195	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}))
35		fveq2 6191	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦))
36	35	oveq2d 6666	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)))
37	34, 36	eqeq12d 2637	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))))
38	30, 37	imbi12d 334	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ (𝑦 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)))))
39	38	imbi2d 330	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝜑 → (𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → (𝑦 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))))))
40		sseq1 3626	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → (𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ↔ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))
41		eleq2 2690	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑓 ↾ 𝐴) ∈ 𝑥 ↔ (𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎})))
42	41	anbi1d 741	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → (((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)))
43	42	abbidv 2741	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} = {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})
44	43	fveq2d 6195	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}))
45		fveq2 6191	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → (#‘𝑥) = (#‘(𝑦 ∪ {𝑎})))
46	45	oveq2d 6666	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))
47	44, 46	eqeq12d 2637	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))
48	40, 47	imbi12d 334	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → ((𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ ((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))))
49	48	imbi2d 330	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑎}) → ((𝜑 → (𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))))
50		sseq1 3626	. . . . . 6 ⊢ (𝑥 = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ↔ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))
51		f1eq1 6096	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑦 → (𝑓:𝐴–1-1→𝐵 ↔ 𝑦:𝐴–1-1→𝐵))
52	51	cbvabv 2747	. . . . . . . . . 10 ⊢ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} = {𝑦 ∣ 𝑦:𝐴–1-1→𝐵}
53	52	eqeq2i 2634	. . . . . . . . 9 ⊢ (𝑥 = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ↔ 𝑥 = {𝑦 ∣ 𝑦:𝐴–1-1→𝐵})
54		ssun1 3776	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧})
55		f1ssres 6108	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 ∧ 𝐴 ⊆ (𝐴 ∪ {𝑧})) → (𝑓 ↾ 𝐴):𝐴–1-1→𝐵)
56	54, 55	mpan2 707	. . . . . . . . . . . . . 14 ⊢ (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 → (𝑓 ↾ 𝐴):𝐴–1-1→𝐵)
57		vex 3203	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
58	57	resex 5443	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ↾ 𝐴) ∈ V
59		f1eq1 6096	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑓 ↾ 𝐴) → (𝑦:𝐴–1-1→𝐵 ↔ (𝑓 ↾ 𝐴):𝐴–1-1→𝐵))
60	58, 59	elab 3350	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ↾ 𝐴) ∈ {𝑦 ∣ 𝑦:𝐴–1-1→𝐵} ↔ (𝑓 ↾ 𝐴):𝐴–1-1→𝐵)
61	56, 60	sylibr 224	. . . . . . . . . . . . 13 ⊢ (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 → (𝑓 ↾ 𝐴) ∈ {𝑦 ∣ 𝑦:𝐴–1-1→𝐵})
62		eleq2 2690	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑦 ∣ 𝑦:𝐴–1-1→𝐵} → ((𝑓 ↾ 𝐴) ∈ 𝑥 ↔ (𝑓 ↾ 𝐴) ∈ {𝑦 ∣ 𝑦:𝐴–1-1→𝐵}))
63	61, 62	syl5ibr 236	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑦 ∣ 𝑦:𝐴–1-1→𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 → (𝑓 ↾ 𝐴) ∈ 𝑥))
64	63	pm4.71rd 667	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑦 ∣ 𝑦:𝐴–1-1→𝐵} → (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 ↔ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)))
65	64	bicomd 213	. . . . . . . . . 10 ⊢ (𝑥 = {𝑦 ∣ 𝑦:𝐴–1-1→𝐵} → (((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵))
66	65	abbidv 2741	. . . . . . . . 9 ⊢ (𝑥 = {𝑦 ∣ 𝑦:𝐴–1-1→𝐵} → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} = {𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵})
67	53, 66	sylbi 207	. . . . . . . 8 ⊢ (𝑥 = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} = {𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵})
68	67	fveq2d 6195	. . . . . . 7 ⊢ (𝑥 = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (#‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}))
69		fveq2 6191	. . . . . . . 8 ⊢ (𝑥 = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘𝑥) = (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))
70	69	oveq2d 6666	. . . . . . 7 ⊢ (𝑥 = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})))
71	68, 70	eqeq12d 2637	. . . . . 6 ⊢ (𝑥 = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)) ↔ (#‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))))
72	50, 71	imbi12d 334	. . . . 5 ⊢ (𝑥 = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → ((𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥))) ↔ ({𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})))))
73	72	imbi2d 330	. . . 4 ⊢ (𝑥 = {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → ((𝜑 → (𝑥 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑥 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑥)))) ↔ (𝜑 → ({𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))))))
74		hashcl 13147	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → (#‘𝐵) ∈ ℕ₀)
75	2, 74	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (#‘𝐵) ∈ ℕ₀)
76	75	nn0cnd 11353	. . . . . . . 8 ⊢ (𝜑 → (#‘𝐵) ∈ ℂ)
77		hashcl 13147	. . . . . . . . . 10 ⊢ (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ₀)
78	3, 77	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (#‘𝐴) ∈ ℕ₀)
79	78	nn0cnd 11353	. . . . . . . 8 ⊢ (𝜑 → (#‘𝐴) ∈ ℂ)
80	76, 79	subcld 10392	. . . . . . 7 ⊢ (𝜑 → ((#‘𝐵) − (#‘𝐴)) ∈ ℂ)
81	80	mul01d 10235	. . . . . 6 ⊢ (𝜑 → (((#‘𝐵) − (#‘𝐴)) · 0) = 0)
82	81	eqcomd 2628	. . . . 5 ⊢ (𝜑 → 0 = (((#‘𝐵) − (#‘𝐴)) · 0))
83	82	a1d 25	. . . 4 ⊢ (𝜑 → (∅ ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → 0 = (((#‘𝐵) − (#‘𝐴)) · 0)))
84		ssun1 3776	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑎})
85		sstr 3611	. . . . . . . . 9 ⊢ ((𝑦 ⊆ (𝑦 ∪ {𝑎}) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) → 𝑦 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})
86	84, 85	mpan 706	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → 𝑦 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})
87	86	imim1i 63	. . . . . . 7 ⊢ ((𝑦 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))))
88		oveq1 6657	. . . . . . . . . 10 ⊢ ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) → ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) + ((#‘𝐵) − (#‘𝐴))) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴))))
89		elun 3753	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∨ (𝑓 ↾ 𝐴) ∈ {𝑎}))
90	58	elsn 4192	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ↾ 𝐴) ∈ {𝑎} ↔ (𝑓 ↾ 𝐴) = 𝑎)
91	90	orbi2i 541	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∨ (𝑓 ↾ 𝐴) ∈ {𝑎}) ↔ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∨ (𝑓 ↾ 𝐴) = 𝑎))
92	89, 91	bitri 264	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ↔ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∨ (𝑓 ↾ 𝐴) = 𝑎))
93	92	anbi1i 731	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∨ (𝑓 ↾ 𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵))
94		andir 912	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑓 ↾ 𝐴) ∈ 𝑦 ∨ (𝑓 ↾ 𝐴) = 𝑎) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∨ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)))
95	93, 94	bitri 264	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∨ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)))
96	95	abbii 2739	. . . . . . . . . . . . . . 15 ⊢ {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} = {𝑓 ∣ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∨ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵))}
97		unab 3894	. . . . . . . . . . . . . . 15 ⊢ ({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∪ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = {𝑓 ∣ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∨ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵))}
98	96, 97	eqtr4i 2647	. . . . . . . . . . . . . 14 ⊢ {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} = ({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∪ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})
99	98	fveq2i 6194	. . . . . . . . . . . . 13 ⊢ (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (#‘({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∪ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}))
100		snfi 8038	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑧} ∈ Fin
101		unfi 8227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
102	3, 100, 101	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
103		mapvalg 7867	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵 ↑_𝑚 (𝐴 ∪ {𝑧})) = {𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
104	2, 102, 103	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 ↑_𝑚 (𝐴 ∪ {𝑧})) = {𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵})
105		mapfi 8262	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ Fin ∧ (𝐴 ∪ {𝑧}) ∈ Fin) → (𝐵 ↑_𝑚 (𝐴 ∪ {𝑧})) ∈ Fin)
106	2, 102, 105	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 ↑_𝑚 (𝐴 ∪ {𝑧})) ∈ Fin)
107	104, 106	eqeltrrd 2702	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin)
108		f1f 6101	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
109	108	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
110	109	ss2abi 3674	. . . . . . . . . . . . . . . 16 ⊢ {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ {𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
111		ssfi 8180	. . . . . . . . . . . . . . . 16 ⊢ (({𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ {𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin)
112	107, 110, 111	sylancl 694	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin)
113	112	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → {𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin)
114	108	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
115	114	ss2abi 3674	. . . . . . . . . . . . . . . 16 ⊢ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ {𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵}
116		ssfi 8180	. . . . . . . . . . . . . . . 16 ⊢ (({𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵} ∈ Fin ∧ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ {𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵}) → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin)
117	107, 115, 116	sylancl 694	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin)
118	117	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin)
119		inab 3895	. . . . . . . . . . . . . . 15 ⊢ ({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∩ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = {𝑓 ∣ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵))}
120		simprlr 803	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → ¬ 𝑎 ∈ 𝑦)
121		abn0 3954	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑓 ∣ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵))} ≠ ∅ ↔ ∃𝑓(((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)))
122		simprl 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑓 ↾ 𝐴) = 𝑎)
123		simpll 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑓 ↾ 𝐴) ∈ 𝑦)
124	122, 123	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝑎 ∈ 𝑦)
125	124	exlimiv 1858	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑓(((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝑎 ∈ 𝑦)
126	121, 125	sylbi 207	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑓 ∣ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵))} ≠ ∅ → 𝑎 ∈ 𝑦)
127	126	necon1bi 2822	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑎 ∈ 𝑦 → {𝑓 ∣ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵))} = ∅)
128	120, 127	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → {𝑓 ∣ (((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵))} = ∅)
129	119, 128	syl5eq 2668	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → ({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∩ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = ∅)
130		hashun 13171	. . . . . . . . . . . . . 14 ⊢ (({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin ∧ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin ∧ ({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∩ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = ∅) → (#‘({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∪ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})) = ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) + (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})))
131	113, 118, 129, 130	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (#‘({𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∪ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})) = ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) + (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})))
132	99, 131	syl5eq 2668	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) + (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})))
133		simpr 477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) → (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})
134	133	unssbd 3791	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) → {𝑎} ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})
135		vex 3203	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ∈ V
136	135	snss 4316	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ↔ {𝑎} ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})
137	134, 136	sylibr 224	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) → 𝑎 ∈ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})
138		f1eq1 6096	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑎 → (𝑓:𝐴–1-1→𝐵 ↔ 𝑎:𝐴–1-1→𝐵))
139	135, 138	elab 3350	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ↔ 𝑎:𝐴–1-1→𝐵)
140	137, 139	sylib 208	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵}) → 𝑎:𝐴–1-1→𝐵)
141	79	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (#‘𝐴) ∈ ℂ)
142	117	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin)
143		hashcl 13147	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ Fin → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) ∈ ℕ₀)
144	142, 143	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) ∈ ℕ₀)
145	144	nn0cnd 11353	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) ∈ ℂ)
146	141, 145	pncan2d 10394	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})) − (#‘𝐴)) = (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}))
147		f1f1orn 6148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎:𝐴–1-1→𝐵 → 𝑎:𝐴–1-1-onto→ran 𝑎)
148	147	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → 𝑎:𝐴–1-1-onto→ran 𝑎)
149		f1oen3g 7971	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ V ∧ 𝑎:𝐴–1-1-onto→ran 𝑎) → 𝐴 ≈ ran 𝑎)
150	135, 148, 149	sylancr 695	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → 𝐴 ≈ ran 𝑎)
151		hasheni 13136	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ≈ ran 𝑎 → (#‘𝐴) = (#‘ran 𝑎))
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (#‘𝐴) = (#‘ran 𝑎))
153	3	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → 𝐴 ∈ Fin)
154	2	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → 𝐵 ∈ Fin)
155		hashf1lem2.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)
156	155	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → ¬ 𝑧 ∈ 𝐴)
157		hashf1lem2.4	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((#‘𝐴) + 1) ≤ (#‘𝐵))
158	157	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → ((#‘𝐴) + 1) ≤ (#‘𝐵))
159		simpr 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → 𝑎:𝐴–1-1→𝐵)
160	153, 154, 156, 158, 159	hashf1lem1 13239	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝑎))
161		hasheni 13136	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝑎) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (#‘(𝐵 ∖ ran 𝑎)))
162	160, 161	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (#‘(𝐵 ∖ ran 𝑎)))
163	152, 162	oveq12d 6668	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → ((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})) = ((#‘ran 𝑎) + (#‘(𝐵 ∖ ran 𝑎))))
164		f1f 6101	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎:𝐴–1-1→𝐵 → 𝑎:𝐴⟶𝐵)
165		frn 6053	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎:𝐴⟶𝐵 → ran 𝑎 ⊆ 𝐵)
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎:𝐴–1-1→𝐵 → ran 𝑎 ⊆ 𝐵)
167	166	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → ran 𝑎 ⊆ 𝐵)
168		ssfi 8180	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ Fin ∧ ran 𝑎 ⊆ 𝐵) → ran 𝑎 ∈ Fin)
169	154, 167, 168	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → ran 𝑎 ∈ Fin)
170		diffi 8192	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ Fin → (𝐵 ∖ ran 𝑎) ∈ Fin)
171	154, 170	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (𝐵 ∖ ran 𝑎) ∈ Fin)
172		disjdif 4040	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅
173	172	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅)
174		hashun 13171	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑎 ∈ Fin ∧ (𝐵 ∖ ran 𝑎) ∈ Fin ∧ (ran 𝑎 ∩ (𝐵 ∖ ran 𝑎)) = ∅) → (#‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((#‘ran 𝑎) + (#‘(𝐵 ∖ ran 𝑎))))
175	169, 171, 173, 174	syl3anc 1326	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (#‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = ((#‘ran 𝑎) + (#‘(𝐵 ∖ ran 𝑎))))
176		undif 4049	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝑎 ⊆ 𝐵 ↔ (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
177	167, 176	sylib 208	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (ran 𝑎 ∪ (𝐵 ∖ ran 𝑎)) = 𝐵)
178	177	fveq2d 6195	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (#‘(ran 𝑎 ∪ (𝐵 ∖ ran 𝑎))) = (#‘𝐵))
179	163, 175, 178	3eqtr2d 2662	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → ((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})) = (#‘𝐵))
180	179	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (((#‘𝐴) + (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})) − (#‘𝐴)) = ((#‘𝐵) − (#‘𝐴)))
181	146, 180	eqtr3d 2658	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎:𝐴–1-1→𝐵) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = ((#‘𝐵) − (#‘𝐴)))
182	140, 181	sylan2 491	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = ((#‘𝐵) − (#‘𝐴)))
183	182	oveq2d 6666	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) + (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝑎 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})) = ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) + ((#‘𝐵) − (#‘𝐴))))
184	132, 183	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) + ((#‘𝐵) − (#‘𝐴))))
185		hashunsng 13181	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑎})) = ((#‘𝑦) + 1)))
186	135, 185	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑎})) = ((#‘𝑦) + 1))
187	186	ad2antrl 764	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (#‘(𝑦 ∪ {𝑎})) = ((#‘𝑦) + 1))
188	187	oveq2d 6666	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))) = (((#‘𝐵) − (#‘𝐴)) · ((#‘𝑦) + 1)))
189	80	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → ((#‘𝐵) − (#‘𝐴)) ∈ ℂ)
190		simprll 802	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → 𝑦 ∈ Fin)
191		hashcl 13147	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Fin → (#‘𝑦) ∈ ℕ₀)
192	190, 191	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (#‘𝑦) ∈ ℕ₀)
193	192	nn0cnd 11353	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (#‘𝑦) ∈ ℂ)
194		1cnd 10056	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → 1 ∈ ℂ)
195	189, 193, 194	adddid 10064	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (((#‘𝐵) − (#‘𝐴)) · ((#‘𝑦) + 1)) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + (((#‘𝐵) − (#‘𝐴)) · 1)))
196	189	mulid1d 10057	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (((#‘𝐵) − (#‘𝐴)) · 1) = ((#‘𝐵) − (#‘𝐴)))
197	196	oveq2d 6666	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + (((#‘𝐵) − (#‘𝐴)) · 1)) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴))))
198	188, 195, 197	3eqtrd 2660	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴))))
199	184, 198	eqeq12d 2637	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))) ↔ ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) + ((#‘𝐵) − (#‘𝐴))) = ((((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) + ((#‘𝐵) − (#‘𝐴)))))
200	88, 199	syl5ibr 236	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) ∧ (𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵})) → ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))
201	200	expr 643	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦)) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → ((#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)) → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))))
202	201	a2d 29	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦)) → (((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))))
203	87, 202	syl5 34	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦)) → ((𝑦 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎}))))))
204	203	expcom 451	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) → (𝜑 → ((𝑦 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦))) → ((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))))
205	204	a2d 29	. . . 4 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑦) → ((𝜑 → (𝑦 ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ 𝑦 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘𝑦)))) → (𝜑 → ((𝑦 ∪ {𝑎}) ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ ((𝑓 ↾ 𝐴) ∈ (𝑦 ∪ {𝑎}) ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) = (((#‘𝐵) − (#‘𝐴)) · (#‘(𝑦 ∪ {𝑎})))))))
206	29, 39, 49, 73, 83, 205	findcard2s 8201	. . 3 ⊢ ({𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ∈ Fin → (𝜑 → ({𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})))))
207	11, 206	mpcom 38	. 2 ⊢ (𝜑 → ({𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ⊆ {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} → (#‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵}))))
208	1, 207	mpi 20	1 ⊢ (𝜑 → (#‘{𝑓 ∣ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵}) = (((#‘𝐵) − (#‘𝐴)) · (#‘{𝑓 ∣ 𝑓:𝐴–1-1→𝐵})))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∨ wo 383 ∧ wa 384 = wceq 1483 ∃wex 1704 ∈ wcel 1990 {cab 2608 ≠ wne 2794 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 {csn 4177 class class class wbr 4653 ran crn 5115 ↾ cres 5116 ⟶wf 5884 –1-1→wf1 5885 –1-1-onto→wf1o 5887 ‘cfv 5888 (class class class)co 6650 ↑_𝑚 cmap 7857 ≈ cen 7952 Fincfn 7955 ℂcc 9934 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 ≤ cle 10075 − cmin 10266 ℕ₀cn0 11292 #chash 13117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-hash 13118

This theorem is referenced by: hashf1 13241

W3C validator