Metamath Proof Explorer

Theorem hashf1

Description: The permutation number | A | ! x. ( | B | _C | A | ) = | B | ! / ( | B | - | A | ) ! counts the number of injections from A to B . (Contributed by Mario Carneiro, 21-Jan-2015)

Ref Expression
Assertion hashf1 ⊢A∈Fin∧B∈Fin→f|f:A⟶1-1B=A!⁢(BA)

Proof

Step Hyp Ref Expression
1 f1eq2 ⊢x=∅→f:x⟶1-1B↔f:∅⟶1-1B
2 f1fn ⊢f:∅⟶1-1B→fFn∅
3 fn0 ⊢fFn∅↔f=∅
4 2 3 sylib ⊢f:∅⟶1-1B→f=∅
5 f10 ⊢∅:∅⟶1-1B
6 f1eq1 ⊢f=∅→f:∅⟶1-1B↔∅:∅⟶1-1B
7 5 6 mpbiri ⊢f=∅→f:∅⟶1-1B
8 4 7 impbii ⊢f:∅⟶1-1B↔f=∅
9 velsn ⊢f∈∅↔f=∅
10 8 9 bitr4i ⊢f:∅⟶1-1B↔f∈∅
11 1 10 bitrdi ⊢x=∅→f:x⟶1-1B↔f∈∅
12 11 eqabcdv ⊢x=∅→f|f:x⟶1-1B=∅
13 12 fveq2d ⊢x=∅→f|f:x⟶1-1B=∅
14 0ex ⊢∅∈V
15 hashsng ⊢∅∈V→∅=1
16 14 15 ax-mp ⊢∅=1
17 13 16 eqtrdi ⊢x=∅→f|f:x⟶1-1B=1
18 fveq2 ⊢x=∅→x=∅
19 hash0 ⊢∅=0
20 18 19 eqtrdi ⊢x=∅→x=0
21 20 fveq2d ⊢x=∅→x!=0!
22 fac0 ⊢0!=1
23 21 22 eqtrdi ⊢x=∅→x!=1
24 20 oveq2d ⊢x=∅→(Bx)=(B0)
25 23 24 oveq12d ⊢x=∅→x!⁢(Bx)=1⁢(B0)
26 17 25 eqeq12d ⊢x=∅→f|f:x⟶1-1B=x!⁢(Bx)↔1=1⁢(B0)
27 26 imbi2d ⊢x=∅→B∈Fin→f|f:x⟶1-1B=x!⁢(Bx)↔B∈Fin→1=1⁢(B0)
28 f1eq2 ⊢x=y→f:x⟶1-1B↔f:y⟶1-1B
29 28 abbidv ⊢x=y→f|f:x⟶1-1B=f|f:y⟶1-1B
30 29 fveq2d ⊢x=y→f|f:x⟶1-1B=f|f:y⟶1-1B
31 2fveq3 ⊢x=y→x!=y!
32 fveq2 ⊢x=y→x=y
33 32 oveq2d ⊢x=y→(Bx)=(By)
34 31 33 oveq12d ⊢x=y→x!⁢(Bx)=y!⁢(By)
35 30 34 eqeq12d ⊢x=y→f|f:x⟶1-1B=x!⁢(Bx)↔f|f:y⟶1-1B=y!⁢(By)
36 35 imbi2d ⊢x=y→B∈Fin→f|f:x⟶1-1B=x!⁢(Bx)↔B∈Fin→f|f:y⟶1-1B=y!⁢(By)
37 f1eq2 ⊢x=y∪z→f:x⟶1-1B↔f:y∪z⟶1-1B
38 37 abbidv ⊢x=y∪z→f|f:x⟶1-1B=f|f:y∪z⟶1-1B
39 38 fveq2d ⊢x=y∪z→f|f:x⟶1-1B=f|f:y∪z⟶1-1B
40 2fveq3 ⊢x=y∪z→x!=y∪z!
41 fveq2 ⊢x=y∪z→x=y∪z
42 41 oveq2d ⊢x=y∪z→(Bx)=(By∪z)
43 40 42 oveq12d ⊢x=y∪z→x!⁢(Bx)=y∪z!⁢(By∪z)
44 39 43 eqeq12d ⊢x=y∪z→f|f:x⟶1-1B=x!⁢(Bx)↔f|f:y∪z⟶1-1B=y∪z!⁢(By∪z)
45 44 imbi2d ⊢x=y∪z→B∈Fin→f|f:x⟶1-1B=x!⁢(Bx)↔B∈Fin→f|f:y∪z⟶1-1B=y∪z!⁢(By∪z)
46 f1eq2 ⊢x=A→f:x⟶1-1B↔f:A⟶1-1B
47 46 abbidv ⊢x=A→f|f:x⟶1-1B=f|f:A⟶1-1B
48 47 fveq2d ⊢x=A→f|f:x⟶1-1B=f|f:A⟶1-1B
49 2fveq3 ⊢x=A→x!=A!
50 fveq2 ⊢x=A→x=A
51 50 oveq2d ⊢x=A→(Bx)=(BA)
52 49 51 oveq12d ⊢x=A→x!⁢(Bx)=A!⁢(BA)
53 48 52 eqeq12d ⊢x=A→f|f:x⟶1-1B=x!⁢(Bx)↔f|f:A⟶1-1B=A!⁢(BA)
54 53 imbi2d ⊢x=A→B∈Fin→f|f:x⟶1-1B=x!⁢(Bx)↔B∈Fin→f|f:A⟶1-1B=A!⁢(BA)
55 hashcl ⊢B∈Fin→B∈ℕ0
56 bcn0 ⊢B∈ℕ0→(B0)=1
57 55 56 syl ⊢B∈Fin→(B0)=1
58 57 oveq2d ⊢B∈Fin→1⁢(B0)=1⋅1
59 1t1e1 ⊢1⋅1=1
60 58 59 eqtr2di ⊢B∈Fin→1=1⁢(B0)
61 abn0 ⊢f|f:y∪z⟶1-1B≠∅↔∃ff:y∪z⟶1-1B
62 f1domg ⊢B∈Fin→f:y∪z⟶1-1B→y∪z≼B
63 62 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y→f:y∪z⟶1-1B→y∪z≼B
64 hashunsng ⊢z∈V→y∈Fin∧¬z∈y→y∪z=y+1
65 64 elv ⊢y∈Fin∧¬z∈y→y∪z=y+1
66 65 adantl ⊢B∈Fin∧y∈Fin∧¬z∈y→y∪z=y+1
67 66 breq1d ⊢B∈Fin∧y∈Fin∧¬z∈y→y∪z≤B↔y+1≤B
68 simprl ⊢B∈Fin∧y∈Fin∧¬z∈y→y∈Fin
69 snfi ⊢z∈Fin
70 unfi ⊢y∈Fin∧z∈Fin→y∪z∈Fin
71 68 69 70 sylancl ⊢B∈Fin∧y∈Fin∧¬z∈y→y∪z∈Fin
72 simpl ⊢B∈Fin∧y∈Fin∧¬z∈y→B∈Fin
73 hashdom ⊢y∪z∈Fin∧B∈Fin→y∪z≤B↔y∪z≼B
74 71 72 73 syl2anc ⊢B∈Fin∧y∈Fin∧¬z∈y→y∪z≤B↔y∪z≼B
75 hashcl ⊢y∈Fin→y∈ℕ0
76 75 ad2antrl ⊢B∈Fin∧y∈Fin∧¬z∈y→y∈ℕ0
77 nn0p1nn ⊢y∈ℕ0→y+1∈ℕ
78 76 77 syl ⊢B∈Fin∧y∈Fin∧¬z∈y→y+1∈ℕ
79 78 nnred ⊢B∈Fin∧y∈Fin∧¬z∈y→y+1∈ℝ
80 55 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y→B∈ℕ0
81 80 nn0red ⊢B∈Fin∧y∈Fin∧¬z∈y→B∈ℝ
82 79 81 lenltd ⊢B∈Fin∧y∈Fin∧¬z∈y→y+1≤B↔¬B<y+1
83 67 74 82 3bitr3d ⊢B∈Fin∧y∈Fin∧¬z∈y→y∪z≼B↔¬B<y+1
84 63 83 sylibd ⊢B∈Fin∧y∈Fin∧¬z∈y→f:y∪z⟶1-1B→¬B<y+1
85 84 exlimdv ⊢B∈Fin∧y∈Fin∧¬z∈y→∃ff:y∪z⟶1-1B→¬B<y+1
86 61 85 biimtrid ⊢B∈Fin∧y∈Fin∧¬z∈y→f|f:y∪z⟶1-1B≠∅→¬B<y+1
87 86 necon4ad ⊢B∈Fin∧y∈Fin∧¬z∈y→B<y+1→f|f:y∪z⟶1-1B=∅
88 87 imp ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→f|f:y∪z⟶1-1B=∅
89 88 fveq2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→f|f:y∪z⟶1-1B=∅
90 hashcl ⊢y∪z∈Fin→y∪z∈ℕ0
91 71 90 syl ⊢B∈Fin∧y∈Fin∧¬z∈y→y∪z∈ℕ0
92 91 faccld ⊢B∈Fin∧y∈Fin∧¬z∈y→y∪z!∈ℕ
93 92 nncnd ⊢B∈Fin∧y∈Fin∧¬z∈y→y∪z!∈ℂ
94 93 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→y∪z!∈ℂ
95 94 mul01d ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→y∪z!⋅0=0
96 19 89 95 3eqtr4a ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→f|f:y∪z⟶1-1B=y∪z!⋅0
97 66 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→y∪z=y+1
98 97 oveq2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→(By∪z)=(By+1)
99 80 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→B∈ℕ0
100 78 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→y+1∈ℕ
101 100 nnzd ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→y+1∈ℤ
102 animorr ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→y+1<0∨B<y+1
103 bcval4 ⊢B∈ℕ0∧y+1∈ℤ∧y+1<0∨B<y+1→(By+1)=0
104 99 101 102 103 syl3anc ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→(By+1)=0
105 98 104 eqtrd ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→(By∪z)=0
106 105 oveq2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→y∪z!⁢(By∪z)=y∪z!⋅0
107 96 106 eqtr4d ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→f|f:y∪z⟶1-1B=y∪z!⁢(By∪z)
108 107 a1d ⊢B∈Fin∧y∈Fin∧¬z∈y∧B<y+1→f|f:y⟶1-1B=y!⁢(By)→f|f:y∪z⟶1-1B=y∪z!⁢(By∪z)
109 oveq2 ⊢f|f:y⟶1-1B=y!⁢(By)→B−y⁢f|f:y⟶1-1B=B−y⁢y!⁢(By)
110 68 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y∈Fin
111 72 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B∈Fin
112 simplrr ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→¬z∈y
113 simpr ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1≤B
114 110 111 112 113 hashf1lem2 ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→f|f:y∪z⟶1-1B=B−y⁢f|f:y⟶1-1B
115 80 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B∈ℕ0
116 115 faccld ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B!∈ℕ
117 116 nncnd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B!∈ℂ
118 76 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y∈ℕ0
119 peano2nn0 ⊢y∈ℕ0→y+1∈ℕ0
120 118 119 syl ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1∈ℕ0
121 nn0sub2 ⊢y+1∈ℕ0∧B∈ℕ0∧y+1≤B→B−y+1∈ℕ0
122 120 115 113 121 syl3anc ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y+1∈ℕ0
123 122 faccld ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y+1!∈ℕ
124 123 nncnd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y+1!∈ℂ
125 123 nnne0d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y+1!≠0
126 117 124 125 divcld ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B!B−y+1!∈ℂ
127 120 faccld ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1!∈ℕ
128 127 nncnd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1!∈ℂ
129 127 nnne0d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1!≠0
130 126 128 129 divcan2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1!⁢B!B−y+1!y+1!=B!B−y+1!
131 115 nn0cnd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B∈ℂ
132 118 nn0cnd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y∈ℂ
133 131 132 subcld ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y∈ℂ
134 ax-1cn ⊢1∈ℂ
135 npcan ⊢B−y∈ℂ∧1∈ℂ→B−y-1+1=B−y
136 133 134 135 sylancl ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y-1+1=B−y
137 1cnd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→1∈ℂ
138 131 132 137 subsub4d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B-y-1=B−y+1
139 138 122 eqeltrd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B-y-1∈ℕ0
140 nn0p1nn ⊢B-y-1∈ℕ0→B−y-1+1∈ℕ
141 139 140 syl ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y-1+1∈ℕ
142 136 141 eqeltrrd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y∈ℕ
143 142 nnne0d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y≠0
144 126 133 143 divcan2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y⁢B!B−y+1!B−y=B!B−y+1!
145 130 144 eqtr4d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1!⁢B!B−y+1!y+1!=B−y⁢B!B−y+1!B−y
146 66 adantr ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y∪z=y+1
147 146 fveq2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y∪z!=y+1!
148 nn0uz ⊢ℕ0=ℤ≥0
149 120 148 eleqtrdi ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1∈ℤ≥0
150 115 nn0zd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B∈ℤ
151 elfz5 ⊢y+1∈ℤ≥0∧B∈ℤ→y+1∈0…B↔y+1≤B
152 149 150 151 syl2anc ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1∈0…B↔y+1≤B
153 113 152 mpbird ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y+1∈0…B
154 bcval2 ⊢y+1∈0…B→(By+1)=B!B−y+1!⁢y+1!
155 153 154 syl ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→(By+1)=B!B−y+1!⁢y+1!
156 146 oveq2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→(By∪z)=(By+1)
157 117 124 128 125 129 divdiv1d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B!B−y+1!y+1!=B!B−y+1!⁢y+1!
158 155 156 157 3eqtr4d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→(By∪z)=B!B−y+1!y+1!
159 147 158 oveq12d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y∪z!⁢(By∪z)=y+1!⁢B!B−y+1!y+1!
160 118 148 eleqtrdi ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y∈ℤ≥0
161 peano2fzr ⊢y∈ℤ≥0∧y+1∈0…B→y∈0…B
162 160 153 161 syl2anc ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y∈0…B
163 bcval2 ⊢y∈0…B→(By)=B!B−y!⁢y!
164 162 163 syl ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→(By)=B!B−y!⁢y!
165 elfzle2 ⊢y∈0…B→y≤B
166 162 165 syl ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y≤B
167 nn0sub2 ⊢y∈ℕ0∧B∈ℕ0∧y≤B→B−y∈ℕ0
168 118 115 166 167 syl3anc ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y∈ℕ0
169 168 faccld ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y!∈ℕ
170 169 nncnd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y!∈ℂ
171 118 faccld ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y!∈ℕ
172 171 nncnd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y!∈ℂ
173 169 nnne0d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y!≠0
174 171 nnne0d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y!≠0
175 117 170 172 173 174 divdiv1d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B!B−y!y!=B!B−y!⁢y!
176 164 175 eqtr4d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→(By)=B!B−y!y!
177 176 oveq2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y!⁢(By)=y!⁢B!B−y!y!
178 facnn2 ⊢B−y∈ℕ→B−y!=B-y-1!⁢B−y
179 142 178 syl ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y!=B-y-1!⁢B−y
180 138 fveq2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B-y-1!=B−y+1!
181 180 oveq1d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B-y-1!⁢B−y=B−y+1!⁢B−y
182 179 181 eqtrd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y!=B−y+1!⁢B−y
183 182 oveq2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B!B−y!=B!B−y+1!⁢B−y
184 117 170 173 divcld ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B!B−y!∈ℂ
185 184 172 174 divcan2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y!⁢B!B−y!y!=B!B−y!
186 117 124 133 125 143 divdiv1d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B!B−y+1!B−y=B!B−y+1!⁢B−y
187 183 185 186 3eqtr4d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y!⁢B!B−y!y!=B!B−y+1!B−y
188 177 187 eqtrd ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y!⁢(By)=B!B−y+1!B−y
189 188 oveq2d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→B−y⁢y!⁢(By)=B−y⁢B!B−y+1!B−y
190 145 159 189 3eqtr4d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→y∪z!⁢(By∪z)=B−y⁢y!⁢(By)
191 114 190 eqeq12d ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→f|f:y∪z⟶1-1B=y∪z!⁢(By∪z)↔B−y⁢f|f:y⟶1-1B=B−y⁢y!⁢(By)
192 109 191 imbitrrid ⊢B∈Fin∧y∈Fin∧¬z∈y∧y+1≤B→f|f:y⟶1-1B=y!⁢(By)→f|f:y∪z⟶1-1B=y∪z!⁢(By∪z)
193 108 192 81 79 ltlecasei ⊢B∈Fin∧y∈Fin∧¬z∈y→f|f:y⟶1-1B=y!⁢(By)→f|f:y∪z⟶1-1B=y∪z!⁢(By∪z)
194 193 expcom ⊢y∈Fin∧¬z∈y→B∈Fin→f|f:y⟶1-1B=y!⁢(By)→f|f:y∪z⟶1-1B=y∪z!⁢(By∪z)
195 194 a2d ⊢y∈Fin∧¬z∈y→B∈Fin→f|f:y⟶1-1B=y!⁢(By)→B∈Fin→f|f:y∪z⟶1-1B=y∪z!⁢(By∪z)
196 27 36 45 54 60 195 findcard2s ⊢A∈Fin→B∈Fin→f|f:A⟶1-1B=A!⁢(BA)
197 196 imp ⊢A∈Fin∧B∈Fin→f|f:A⟶1-1B=A!⁢(BA)