Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝑥 = ∅ → ( ( 𝑓 ↾ 𝐴 ) ∈ 𝑥 → 𝑓 ∈ ∅ ) )
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→ 𝐵 } ) ) )