Theorem prprelb

Description: An element of the set of all proper unordered pairs over a given set V is a subset of V of size two. (Contributed by AV, 29-Apr-2023)

	Ref	Expression
Assertion	prprelb	|- ( V e. W -> ( P e. ( PrPairs ` V ) <-> ( P e. ~P V /\ ( # ` P ) = 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prprvalpw	|- ( V e. W -> ( PrPairs ` V ) = { p e. ~P V | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } )
2	1	eleq2d	|- ( V e. W -> ( P e. ( PrPairs ` V ) <-> P e. { p e. ~P V | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } ) )
3		eqeq1	|- ( p = P -> ( p = { a , b } <-> P = { a , b } ) )
4	3	anbi2d	|- ( p = P -> ( ( a =/= b /\ p = { a , b } ) <-> ( a =/= b /\ P = { a , b } ) ) )
5	4	2rexbidv	|- ( p = P -> ( E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) <-> E. a e. V E. b e. V ( a =/= b /\ P = { a , b } ) ) )
6	5	elrab	|- ( P e. { p e. ~P V | E. a e. V E. b e. V ( a =/= b /\ p = { a , b } ) } <-> ( P e. ~P V /\ E. a e. V E. b e. V ( a =/= b /\ P = { a , b } ) ) )
7	2 6	bitrdi	|- ( V e. W -> ( P e. ( PrPairs ` V ) <-> ( P e. ~P V /\ E. a e. V E. b e. V ( a =/= b /\ P = { a , b } ) ) ) )
8		hash2exprb	|- ( P e. ~P V -> ( ( # ` P ) = 2 <-> E. a E. b ( a =/= b /\ P = { a , b } ) ) )
9		eleq1	|- ( P = { a , b } -> ( P e. ~P V <-> { a , b } e. ~P V ) )
10		prelpw	|- ( ( a e. _V /\ b e. _V ) -> ( ( a e. V /\ b e. V ) <-> { a , b } e. ~P V ) )
11	10	el2v	|- ( ( a e. V /\ b e. V ) <-> { a , b } e. ~P V )
12	11	biimpri	|- ( { a , b } e. ~P V -> ( a e. V /\ b e. V ) )
13	9 12	syl6bi	|- ( P = { a , b } -> ( P e. ~P V -> ( a e. V /\ b e. V ) ) )
14	13	com12	|- ( P e. ~P V -> ( P = { a , b } -> ( a e. V /\ b e. V ) ) )
15	14	adantld	|- ( P e. ~P V -> ( ( a =/= b /\ P = { a , b } ) -> ( a e. V /\ b e. V ) ) )
16	15	pm4.71rd	|- ( P e. ~P V -> ( ( a =/= b /\ P = { a , b } ) <-> ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ P = { a , b } ) ) ) )
17	16	2exbidv	|- ( P e. ~P V -> ( E. a E. b ( a =/= b /\ P = { a , b } ) <-> E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ P = { a , b } ) ) ) )
18		r2ex	|- ( E. a e. V E. b e. V ( a =/= b /\ P = { a , b } ) <-> E. a E. b ( ( a e. V /\ b e. V ) /\ ( a =/= b /\ P = { a , b } ) ) )
19	17 18	bitr4di	|- ( P e. ~P V -> ( E. a E. b ( a =/= b /\ P = { a , b } ) <-> E. a e. V E. b e. V ( a =/= b /\ P = { a , b } ) ) )
20	8 19	bitr2d	|- ( P e. ~P V -> ( E. a e. V E. b e. V ( a =/= b /\ P = { a , b } ) <-> ( # ` P ) = 2 ) )
21	20	pm5.32i	|- ( ( P e. ~P V /\ E. a e. V E. b e. V ( a =/= b /\ P = { a , b } ) ) <-> ( P e. ~P V /\ ( # ` P ) = 2 ) )
22	7 21	bitrdi	|- ( V e. W -> ( P e. ( PrPairs ` V ) <-> ( P e. ~P V /\ ( # ` P ) = 2 ) ) )