| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-tp |
|- { 0 , 1 , 2 } = ( { 0 , 1 } u. { 2 } ) |
| 2 |
1
|
fveq2i |
|- ( # ` { 0 , 1 , 2 } ) = ( # ` ( { 0 , 1 } u. { 2 } ) ) |
| 3 |
|
prfi |
|- { 0 , 1 } e. Fin |
| 4 |
|
snfi |
|- { 2 } e. Fin |
| 5 |
|
2ne0 |
|- 2 =/= 0 |
| 6 |
|
1ne2 |
|- 1 =/= 2 |
| 7 |
6
|
necomi |
|- 2 =/= 1 |
| 8 |
5 7
|
nelpri |
|- -. 2 e. { 0 , 1 } |
| 9 |
|
disjsn |
|- ( ( { 0 , 1 } i^i { 2 } ) = (/) <-> -. 2 e. { 0 , 1 } ) |
| 10 |
8 9
|
mpbir |
|- ( { 0 , 1 } i^i { 2 } ) = (/) |
| 11 |
|
hashun |
|- ( ( { 0 , 1 } e. Fin /\ { 2 } e. Fin /\ ( { 0 , 1 } i^i { 2 } ) = (/) ) -> ( # ` ( { 0 , 1 } u. { 2 } ) ) = ( ( # ` { 0 , 1 } ) + ( # ` { 2 } ) ) ) |
| 12 |
3 4 10 11
|
mp3an |
|- ( # ` ( { 0 , 1 } u. { 2 } ) ) = ( ( # ` { 0 , 1 } ) + ( # ` { 2 } ) ) |
| 13 |
2 12
|
eqtri |
|- ( # ` { 0 , 1 , 2 } ) = ( ( # ` { 0 , 1 } ) + ( # ` { 2 } ) ) |
| 14 |
|
prhash2ex |
|- ( # ` { 0 , 1 } ) = 2 |
| 15 |
|
2z |
|- 2 e. ZZ |
| 16 |
|
hashsng |
|- ( 2 e. ZZ -> ( # ` { 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 |