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