Step |
Hyp |
Ref |
Expression |
1 |
|
3nn0 |
|- 3 e. NN0 |
2 |
|
hashvnfin |
|- ( ( V e. W /\ 3 e. NN0 ) -> ( ( # ` V ) = 3 -> V e. Fin ) ) |
3 |
1 2
|
mpan2 |
|- ( V e. W -> ( ( # ` V ) = 3 -> V e. Fin ) ) |
4 |
3
|
imp |
|- ( ( V e. W /\ ( # ` V ) = 3 ) -> V e. Fin ) |
5 |
|
hash3 |
|- ( # ` 3o ) = 3 |
6 |
5
|
eqcomi |
|- 3 = ( # ` 3o ) |
7 |
6
|
a1i |
|- ( V e. Fin -> 3 = ( # ` 3o ) ) |
8 |
7
|
eqeq2d |
|- ( V e. Fin -> ( ( # ` V ) = 3 <-> ( # ` V ) = ( # ` 3o ) ) ) |
9 |
|
3onn |
|- 3o e. _om |
10 |
|
nnfi |
|- ( 3o e. _om -> 3o e. Fin ) |
11 |
9 10
|
ax-mp |
|- 3o e. Fin |
12 |
|
hashen |
|- ( ( V e. Fin /\ 3o e. Fin ) -> ( ( # ` V ) = ( # ` 3o ) <-> V ~~ 3o ) ) |
13 |
11 12
|
mpan2 |
|- ( V e. Fin -> ( ( # ` V ) = ( # ` 3o ) <-> V ~~ 3o ) ) |
14 |
13
|
biimpd |
|- ( V e. Fin -> ( ( # ` V ) = ( # ` 3o ) -> V ~~ 3o ) ) |
15 |
8 14
|
sylbid |
|- ( V e. Fin -> ( ( # ` V ) = 3 -> V ~~ 3o ) ) |
16 |
15
|
adantld |
|- ( V e. Fin -> ( ( V e. W /\ ( # ` V ) = 3 ) -> V ~~ 3o ) ) |
17 |
4 16
|
mpcom |
|- ( ( V e. W /\ ( # ` V ) = 3 ) -> V ~~ 3o ) |
18 |
|
en3 |
|- ( V ~~ 3o -> E. a E. b E. c V = { a , b , c } ) |
19 |
17 18
|
syl |
|- ( ( V e. W /\ ( # ` V ) = 3 ) -> E. a E. b E. c V = { a , b , c } ) |