Theorem hashf1lem2

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

	Ref	Expression
Hypotheses	hashf1lem2.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	hashf1lem2.2	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	hashf1lem2.3	⊢ ( 𝜑 → ¬ 𝑧 ∈ 𝐴 )
	hashf1lem2.4	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) + 1 ) ≤ ( ♯ ‘ 𝐵 ) )
Assertion	hashf1lem2	⊢ ( 𝜑 → ( ♯ ‘ { 𝑓 ∣ 𝑓 : ( 𝐴 ∪ { 𝑧 } ) –1-1→ 𝐵 } ) = ( ( ( ♯ ‘ 𝐵 ) − ( ♯ ‘ 𝐴 ) ) · ( ♯ ‘ { 𝑓 ∣ 𝑓 : 𝐴 –1-1→ 𝐵 } ) ) )

Proof

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