This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashle2pr

Description: A nonempty set of size less than or equal to two is an unordered pair of sets. (Contributed by AV, 24-Nov-2021)

Ref Expression
Assertion hashle2pr 
|- ( ( P e. V /\ P =/= (/) ) -> ( ( # ` P ) <_ 2 <-> E. a E. b P = { a , b } ) )

Proof

Step Hyp Ref Expression
1 hashxnn0 
 |-  ( P e. V -> ( # ` P ) e. NN0* )
2 xnn0le2is012 
 |-  ( ( ( # ` P ) e. NN0* /\ ( # ` P ) <_ 2 ) -> ( ( # ` P ) = 0 \/ ( # ` P ) = 1 \/ ( # ` P ) = 2 ) )
3 1 2 sylan 
 |-  ( ( P e. V /\ ( # ` P ) <_ 2 ) -> ( ( # ` P ) = 0 \/ ( # ` P ) = 1 \/ ( # ` P ) = 2 ) )
4 3 ex 
 |-  ( P e. V -> ( ( # ` P ) <_ 2 -> ( ( # ` P ) = 0 \/ ( # ` P ) = 1 \/ ( # ` P ) = 2 ) ) )
5 hasheq0 
 |-  ( P e. V -> ( ( # ` P ) = 0 <-> P = (/) ) )
6 eqneqall 
 |-  ( P = (/) -> ( P =/= (/) -> E. a E. b P = { a , b } ) )
7 5 6 biimtrdi 
 |-  ( P e. V -> ( ( # ` P ) = 0 -> ( P =/= (/) -> E. a E. b P = { a , b } ) ) )
8 7 com12 
 |-  ( ( # ` P ) = 0 -> ( P e. V -> ( P =/= (/) -> E. a E. b P = { a , b } ) ) )
9 hash1snb 
 |-  ( P e. V -> ( ( # ` P ) = 1 <-> E. c P = { c } ) )
10 vex 
 |-  c e. _V
11 preq12 
 |-  ( ( a = c /\ b = c ) -> { a , b } = { c , c } )
12 dfsn2 
 |-  { c } = { c , c }
13 11 12 eqtr4di 
 |-  ( ( a = c /\ b = c ) -> { a , b } = { c } )
14 13 eqeq2d 
 |-  ( ( a = c /\ b = c ) -> ( P = { a , b } <-> P = { c } ) )
15 10 10 14 spc2ev 
 |-  ( P = { c } -> E. a E. b P = { a , b } )
16 15 exlimiv 
 |-  ( E. c P = { c } -> E. a E. b P = { a , b } )
17 9 16 biimtrdi 
 |-  ( P e. V -> ( ( # ` P ) = 1 -> E. a E. b P = { a , b } ) )
18 17 imp 
 |-  ( ( P e. V /\ ( # ` P ) = 1 ) -> E. a E. b P = { a , b } )
19 18 a1d 
 |-  ( ( P e. V /\ ( # ` P ) = 1 ) -> ( P =/= (/) -> E. a E. b P = { a , b } ) )
20 19 expcom 
 |-  ( ( # ` P ) = 1 -> ( P e. V -> ( P =/= (/) -> E. a E. b P = { a , b } ) ) )
21 hash2pr 
 |-  ( ( P e. V /\ ( # ` P ) = 2 ) -> E. a E. b P = { a , b } )
22 21 a1d 
 |-  ( ( P e. V /\ ( # ` P ) = 2 ) -> ( P =/= (/) -> E. a E. b P = { a , b } ) )
23 22 expcom 
 |-  ( ( # ` P ) = 2 -> ( P e. V -> ( P =/= (/) -> E. a E. b P = { a , b } ) ) )
24 8 20 23 3jaoi 
 |-  ( ( ( # ` P ) = 0 \/ ( # ` P ) = 1 \/ ( # ` P ) = 2 ) -> ( P e. V -> ( P =/= (/) -> E. a E. b P = { a , b } ) ) )
25 24 com12 
 |-  ( P e. V -> ( ( ( # ` P ) = 0 \/ ( # ` P ) = 1 \/ ( # ` P ) = 2 ) -> ( P =/= (/) -> E. a E. b P = { a , b } ) ) )
26 4 25 syld 
 |-  ( P e. V -> ( ( # ` P ) <_ 2 -> ( P =/= (/) -> E. a E. b P = { a , b } ) ) )
27 26 com23 
 |-  ( P e. V -> ( P =/= (/) -> ( ( # ` P ) <_ 2 -> E. a E. b P = { a , b } ) ) )
28 27 imp 
 |-  ( ( P e. V /\ P =/= (/) ) -> ( ( # ` P ) <_ 2 -> E. a E. b P = { a , b } ) )
29 fveq2 
 |-  ( P = { a , b } -> ( # ` P ) = ( # ` { a , b } ) )
30 hashprlei 
 |-  ( { a , b } e. Fin /\ ( # ` { a , b } ) <_ 2 )
31 30 simpri 
 |-  ( # ` { a , b } ) <_ 2
32 29 31 eqbrtrdi 
 |-  ( P = { a , b } -> ( # ` P ) <_ 2 )
33 32 exlimivv 
 |-  ( E. a E. b P = { a , b } -> ( # ` P ) <_ 2 )
34 28 33 impbid1 
 |-  ( ( P e. V /\ P =/= (/) ) -> ( ( # ` P ) <_ 2 <-> E. a E. b P = { a , b } ) )