Step |
Hyp |
Ref |
Expression |
1 |
|
df-tp |
⊢ { 0 , 1 , 2 } = ( { 0 , 1 } ∪ { 2 } ) |
2 |
1
|
fveq2i |
⊢ ( ♯ ‘ { 0 , 1 , 2 } ) = ( ♯ ‘ ( { 0 , 1 } ∪ { 2 } ) ) |
3 |
|
prfi |
⊢ { 0 , 1 } ∈ Fin |
4 |
|
snfi |
⊢ { 2 } ∈ Fin |
5 |
|
2ne0 |
⊢ 2 ≠ 0 |
6 |
|
1ne2 |
⊢ 1 ≠ 2 |
7 |
6
|
necomi |
⊢ 2 ≠ 1 |
8 |
5 7
|
nelpri |
⊢ ¬ 2 ∈ { 0 , 1 } |
9 |
|
disjsn |
⊢ ( ( { 0 , 1 } ∩ { 2 } ) = ∅ ↔ ¬ 2 ∈ { 0 , 1 } ) |
10 |
8 9
|
mpbir |
⊢ ( { 0 , 1 } ∩ { 2 } ) = ∅ |
11 |
|
hashun |
⊢ ( ( { 0 , 1 } ∈ Fin ∧ { 2 } ∈ Fin ∧ ( { 0 , 1 } ∩ { 2 } ) = ∅ ) → ( ♯ ‘ ( { 0 , 1 } ∪ { 2 } ) ) = ( ( ♯ ‘ { 0 , 1 } ) + ( ♯ ‘ { 2 } ) ) ) |
12 |
3 4 10 11
|
mp3an |
⊢ ( ♯ ‘ ( { 0 , 1 } ∪ { 2 } ) ) = ( ( ♯ ‘ { 0 , 1 } ) + ( ♯ ‘ { 2 } ) ) |
13 |
2 12
|
eqtri |
⊢ ( ♯ ‘ { 0 , 1 , 2 } ) = ( ( ♯ ‘ { 0 , 1 } ) + ( ♯ ‘ { 2 } ) ) |
14 |
|
prhash2ex |
⊢ ( ♯ ‘ { 0 , 1 } ) = 2 |
15 |
|
2z |
⊢ 2 ∈ ℤ |
16 |
|
hashsng |
⊢ ( 2 ∈ ℤ → ( ♯ ‘ { 2 } ) = 1 ) |
17 |
15 16
|
ax-mp |
⊢ ( ♯ ‘ { 2 } ) = 1 |
18 |
14 17
|
oveq12i |
⊢ ( ( ♯ ‘ { 0 , 1 } ) + ( ♯ ‘ { 2 } ) ) = ( 2 + 1 ) |
19 |
|
2p1e3 |
⊢ ( 2 + 1 ) = 3 |
20 |
18 19
|
eqtri |
⊢ ( ( ♯ ‘ { 0 , 1 } ) + ( ♯ ‘ { 2 } ) ) = 3 |
21 |
13 20
|
eqtri |
⊢ ( ♯ ‘ { 0 , 1 , 2 } ) = 3 |