Theorem hash2pr

Description: A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017)

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

Proof

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