Theorem hash3tr

Description: A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018)

	Ref	Expression
Assertion	hash3tr	|- ( ( V e. W /\ ( # ` V ) = 3 ) -> E. a E. b E. c V = { a , b , c } )

Proof

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 } )