prprelprb

Description: A set is an element of the set of all proper unordered pairs over a given set X iff it is a pair of different elements of the set X . (Contributed by AV, 7-May-2023)

		Ref	Expression
	Assertion	prprelprb	$⊢ P \in PrPairs (X) \leftrightarrow (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b))$

Proof

Step	Hyp	Ref	Expression
1		prprvalpw	$⊢ X \in V \to PrPairs (X) = \{p \in 𝒫 X \| \exists a \in X \exists b \in X (a \neq b \land p = \{a, b\})\}$
2	1	eleq2d	$⊢ X \in V \to (P \in PrPairs (X) \leftrightarrow P \in \{p \in 𝒫 X \| \exists a \in X \exists b \in X (a \neq b \land p = \{a, b\})\})$
3		eqeq1	$⊢ p = P \to (p = \{a, b\} \leftrightarrow P = \{a, b\})$
4	3	anbi2d	$⊢ p = P \to ((a \neq b \land p = \{a, b\}) \leftrightarrow (a \neq b \land P = \{a, b\}))$
5	4	2rexbidv	$⊢ p = P \to (\exists a \in X \exists b \in X (a \neq b \land p = \{a, b\}) \leftrightarrow \exists a \in X \exists b \in X (a \neq b \land P = \{a, b\}))$
6	5	elrab	$⊢ P \in \{p \in 𝒫 X \| \exists a \in X \exists b \in X (a \neq b \land p = \{a, b\})\} \leftrightarrow (P \in 𝒫 X \land \exists a \in X \exists b \in X (a \neq b \land P = \{a, b\}))$
7	2 6	syl6bb	$⊢ X \in V \to (P \in PrPairs (X) \leftrightarrow (P \in 𝒫 X \land \exists a \in X \exists b \in X (a \neq b \land P = \{a, b\})))$
8		pm3.22	$⊢ (a \neq b \land P = \{a, b\}) \to (P = \{a, b\} \land a \neq b)$
9	8	a1i	$⊢ (P \in 𝒫 X \land (a \in X \land b \in X)) \to ((a \neq b \land P = \{a, b\}) \to (P = \{a, b\} \land a \neq b))$
10	9	reximdvva	$⊢ P \in 𝒫 X \to (\exists a \in X \exists b \in X (a \neq b \land P = \{a, b\}) \to \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b))$
11	10	imp	$⊢ (P \in 𝒫 X \land \exists a \in X \exists b \in X (a \neq b \land P = \{a, b\})) \to \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)$
12	11	anim2i	$⊢ (X \in V \land (P \in 𝒫 X \land \exists a \in X \exists b \in X (a \neq b \land P = \{a, b\}))) \to (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b))$
13	12	ex	$⊢ X \in V \to ((P \in 𝒫 X \land \exists a \in X \exists b \in X (a \neq b \land P = \{a, b\})) \to (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)))$
14		simpr	$⊢ ((X \in V \land (a \in X \land b \in X)) \land (P = \{a, b\} \land a \neq b)) \to (P = \{a, b\} \land a \neq b)$
15	14	ancomd	$⊢ ((X \in V \land (a \in X \land b \in X)) \land (P = \{a, b\} \land a \neq b)) \to (a \neq b \land P = \{a, b\})$
16		prelpwi	$⊢ (a \in X \land b \in X) \to \{a, b\} \in 𝒫 X$
17	16	adantl	$⊢ (X \in V \land (a \in X \land b \in X)) \to \{a, b\} \in 𝒫 X$
18	17	adantr	$⊢ ((X \in V \land (a \in X \land b \in X)) \land (P = \{a, b\} \land a \neq b)) \to \{a, b\} \in 𝒫 X$
19		eleq1	$⊢ P = \{a, b\} \to (P \in 𝒫 X \leftrightarrow \{a, b\} \in 𝒫 X)$
20	19	adantr	$⊢ (P = \{a, b\} \land a \neq b) \to (P \in 𝒫 X \leftrightarrow \{a, b\} \in 𝒫 X)$
21	20	adantl	$⊢ ((X \in V \land (a \in X \land b \in X)) \land (P = \{a, b\} \land a \neq b)) \to (P \in 𝒫 X \leftrightarrow \{a, b\} \in 𝒫 X)$
22	18 21	mpbird	$⊢ ((X \in V \land (a \in X \land b \in X)) \land (P = \{a, b\} \land a \neq b)) \to P \in 𝒫 X$
23	15 22	jca	$⊢ ((X \in V \land (a \in X \land b \in X)) \land (P = \{a, b\} \land a \neq b)) \to ((a \neq b \land P = \{a, b\}) \land P \in 𝒫 X)$
24	23	ex	$⊢ (X \in V \land (a \in X \land b \in X)) \to ((P = \{a, b\} \land a \neq b) \to ((a \neq b \land P = \{a, b\}) \land P \in 𝒫 X))$
25	24	reximdvva	$⊢ X \in V \to (\exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b) \to \exists a \in X \exists b \in X ((a \neq b \land P = \{a, b\}) \land P \in 𝒫 X))$
26	25	imp	$⊢ (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)) \to \exists a \in X \exists b \in X ((a \neq b \land P = \{a, b\}) \land P \in 𝒫 X)$
27		r19.41vv	$⊢ \exists a \in X \exists b \in X ((a \neq b \land P = \{a, b\}) \land P \in 𝒫 X) \leftrightarrow (\exists a \in X \exists b \in X (a \neq b \land P = \{a, b\}) \land P \in 𝒫 X)$
28	27	biancomi	$⊢ \exists a \in X \exists b \in X ((a \neq b \land P = \{a, b\}) \land P \in 𝒫 X) \leftrightarrow (P \in 𝒫 X \land \exists a \in X \exists b \in X (a \neq b \land P = \{a, b\}))$
29	26 28	sylib	$⊢ (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)) \to (P \in 𝒫 X \land \exists a \in X \exists b \in X (a \neq b \land P = \{a, b\}))$
30	13 29	impbid1	$⊢ X \in V \to ((P \in 𝒫 X \land \exists a \in X \exists b \in X (a \neq b \land P = \{a, b\})) \leftrightarrow (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)))$
31	7 30	bitrd	$⊢ X \in V \to (P \in PrPairs (X) \leftrightarrow (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)))$
32		fvprc	$⊢ \neg X \in V \to PrPairs (X) = \emptyset$
33	32	eleq2d	$⊢ \neg X \in V \to (P \in PrPairs (X) \leftrightarrow P \in \emptyset)$
34		noel	$⊢ \neg P \in \emptyset$
35		pm2.21	$⊢ \neg P \in \emptyset \to (P \in \emptyset \to (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)))$
36	34 35	mp1i	$⊢ \neg X \in V \to (P \in \emptyset \to (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)))$
37		pm2.21	$⊢ \neg X \in V \to (X \in V \to (\exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b) \to P \in \emptyset))$
38	37	impd	$⊢ \neg X \in V \to ((X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)) \to P \in \emptyset)$
39	36 38	impbid	$⊢ \neg X \in V \to (P \in \emptyset \leftrightarrow (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)))$
40	33 39	bitrd	$⊢ \neg X \in V \to (P \in PrPairs (X) \leftrightarrow (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b)))$
41	31 40	pm2.61i	$⊢ P \in PrPairs (X) \leftrightarrow (X \in V \land \exists a \in X \exists b \in X (P = \{a, b\} \land a \neq b))$

Metamath Proof Explorer

Theorem prprelprb

Proof