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

Metamath Proof Explorer

Theorem hashle2prv

Description: A nonempty subset of a powerset of a class V has size less than or equal to two iff it is an unordered pair of elements of V . (Contributed by AV, 24-Nov-2021)

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

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( P e. ( ~P V \ { (/) } ) <-> ( P e. ~P V /\ P =/= (/) ) )
2 hashle2pr 
 |-  ( ( P e. ~P V /\ P =/= (/) ) -> ( ( # ` P ) <_ 2 <-> E. a E. b P = { a , b } ) )
3 1 2 sylbi 
 |-  ( P e. ( ~P V \ { (/) } ) -> ( ( # ` P ) <_ 2 <-> E. a E. b P = { a , b } ) )
4 eldifi 
 |-  ( P e. ( ~P V \ { (/) } ) -> P e. ~P V )
5 eleq1 
 |-  ( P = { a , b } -> ( P e. ~P V <-> { a , b } e. ~P V ) )
6 prelpw 
 |-  ( ( a e. _V /\ b e. _V ) -> ( ( a e. V /\ b e. V ) <-> { a , b } e. ~P V ) )
7 6 biimprd 
 |-  ( ( a e. _V /\ b e. _V ) -> ( { a , b } e. ~P V -> ( a e. V /\ b e. V ) ) )
8 7 el2v 
 |-  ( { a , b } e. ~P V -> ( a e. V /\ b e. V ) )
9 5 8 biimtrdi 
 |-  ( P = { a , b } -> ( P e. ~P V -> ( a e. V /\ b e. V ) ) )
10 4 9 syl5com 
 |-  ( P e. ( ~P V \ { (/) } ) -> ( P = { a , b } -> ( a e. V /\ b e. V ) ) )
11 10 pm4.71rd 
 |-  ( P e. ( ~P V \ { (/) } ) -> ( P = { a , b } <-> ( ( a e. V /\ b e. V ) /\ P = { a , b } ) ) )
12 11 2exbidv 
 |-  ( P e. ( ~P V \ { (/) } ) -> ( E. a E. b P = { a , b } <-> E. a E. b ( ( a e. V /\ b e. V ) /\ P = { a , b } ) ) )
13 r2ex 
 |-  ( E. a e. V E. b e. V P = { a , b } <-> E. a E. b ( ( a e. V /\ b e. V ) /\ P = { a , b } ) )
14 13 bicomi 
 |-  ( E. a E. b ( ( a e. V /\ b e. V ) /\ P = { a , b } ) <-> E. a e. V E. b e. V P = { a , b } )
15 14 a1i 
 |-  ( P e. ( ~P V \ { (/) } ) -> ( E. a E. b ( ( a e. V /\ b e. V ) /\ P = { a , b } ) <-> E. a e. V E. b e. V P = { a , b } ) )
16 3 12 15 3bitrd 
 |-  ( P e. ( ~P V \ { (/) } ) -> ( ( # ` P ) <_ 2 <-> E. a e. V E. b e. V P = { a , b } ) )