Step |
Hyp |
Ref |
Expression |
1 |
|
derang.d |
⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) ) |
2 |
|
snfi |
⊢ { 𝐴 } ∈ Fin |
3 |
1
|
derangval |
⊢ ( { 𝐴 } ∈ Fin → ( 𝐷 ‘ { 𝐴 } ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) ) |
4 |
2 3
|
ax-mp |
⊢ ( 𝐷 ‘ { 𝐴 } ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) |
5 |
|
f1of |
⊢ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } → 𝑓 : { 𝐴 } ⟶ { 𝐴 } ) |
6 |
5
|
adantr |
⊢ ( ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) → 𝑓 : { 𝐴 } ⟶ { 𝐴 } ) |
7 |
|
snidg |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } ) |
8 |
|
ffvelrn |
⊢ ( ( 𝑓 : { 𝐴 } ⟶ { 𝐴 } ∧ 𝐴 ∈ { 𝐴 } ) → ( 𝑓 ‘ 𝐴 ) ∈ { 𝐴 } ) |
9 |
6 7 8
|
syl2anr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ) → ( 𝑓 ‘ 𝐴 ) ∈ { 𝐴 } ) |
10 |
|
simpr |
⊢ ( ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) → ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) |
11 |
|
fveq2 |
⊢ ( 𝑦 = 𝐴 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝐴 ) ) |
12 |
|
id |
⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 ) |
13 |
11 12
|
neeq12d |
⊢ ( 𝑦 = 𝐴 → ( ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ↔ ( 𝑓 ‘ 𝐴 ) ≠ 𝐴 ) ) |
14 |
13
|
rspcva |
⊢ ( ( 𝐴 ∈ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) → ( 𝑓 ‘ 𝐴 ) ≠ 𝐴 ) |
15 |
7 10 14
|
syl2an |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ) → ( 𝑓 ‘ 𝐴 ) ≠ 𝐴 ) |
16 |
|
nelsn |
⊢ ( ( 𝑓 ‘ 𝐴 ) ≠ 𝐴 → ¬ ( 𝑓 ‘ 𝐴 ) ∈ { 𝐴 } ) |
17 |
15 16
|
syl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ) → ¬ ( 𝑓 ‘ 𝐴 ) ∈ { 𝐴 } ) |
18 |
9 17
|
pm2.21dd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) ) → 𝑓 ∈ ∅ ) |
19 |
18
|
ex |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) → 𝑓 ∈ ∅ ) ) |
20 |
19
|
abssdv |
⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ⊆ ∅ ) |
21 |
|
ss0 |
⊢ ( { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ⊆ ∅ → { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } = ∅ ) |
22 |
20 21
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } = ∅ ) |
23 |
22
|
fveq2d |
⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : { 𝐴 } –1-1-onto→ { 𝐴 } ∧ ∀ 𝑦 ∈ { 𝐴 } ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) = ( ♯ ‘ ∅ ) ) |
24 |
4 23
|
syl5eq |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐷 ‘ { 𝐴 } ) = ( ♯ ‘ ∅ ) ) |
25 |
|
hash0 |
⊢ ( ♯ ‘ ∅ ) = 0 |
26 |
24 25
|
eqtrdi |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐷 ‘ { 𝐴 } ) = 0 ) |