elss2prb

Description: An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020)

		Ref	Expression
	Assertion	elss2prb	$⊢ P \in \{z \in 𝒫 V \| \|z\| = 2\} \leftrightarrow \exists x \in V \exists y \in V (x \neq y \land P = \{x, y\})$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$⊢ z = P \to (\|z\| = 2 \leftrightarrow \|P\| = 2)$
2	1	elrab	$⊢ P \in \{z \in 𝒫 V \| \|z\| = 2\} \leftrightarrow (P \in 𝒫 V \land \|P\| = 2)$
3		hash2prb	$⊢ P \in 𝒫 V \to (\|P\| = 2 \leftrightarrow \exists x \in P \exists y \in P (x \neq y \land P = \{x, y\}))$
4		elpwi	$⊢ P \in 𝒫 V \to P \subseteq V$
5		ssrexv	$⊢ P \subseteq V \to (\exists x \in P \exists y \in P (x \neq y \land P = \{x, y\}) \to \exists x \in V \exists y \in P (x \neq y \land P = \{x, y\}))$
6	4 5	syl	$⊢ P \in 𝒫 V \to (\exists x \in P \exists y \in P (x \neq y \land P = \{x, y\}) \to \exists x \in V \exists y \in P (x \neq y \land P = \{x, y\}))$
7		ssrexv	$⊢ P \subseteq V \to (\exists y \in P (x \neq y \land P = \{x, y\}) \to \exists y \in V (x \neq y \land P = \{x, y\}))$
8	4 7	syl	$⊢ P \in 𝒫 V \to (\exists y \in P (x \neq y \land P = \{x, y\}) \to \exists y \in V (x \neq y \land P = \{x, y\}))$
9	8	reximdv	$⊢ P \in 𝒫 V \to (\exists x \in V \exists y \in P (x \neq y \land P = \{x, y\}) \to \exists x \in V \exists y \in V (x \neq y \land P = \{x, y\}))$
10	6 9	syld	$⊢ P \in 𝒫 V \to (\exists x \in P \exists y \in P (x \neq y \land P = \{x, y\}) \to \exists x \in V \exists y \in V (x \neq y \land P = \{x, y\}))$
11	3 10	sylbid	$⊢ P \in 𝒫 V \to (\|P\| = 2 \to \exists x \in V \exists y \in V (x \neq y \land P = \{x, y\}))$
12	11	imp	$⊢ (P \in 𝒫 V \land \|P\| = 2) \to \exists x \in V \exists y \in V (x \neq y \land P = \{x, y\})$
13		prelpwi	$⊢ (x \in V \land y \in V) \to \{x, y\} \in 𝒫 V$
14	13	adantr	$⊢ ((x \in V \land y \in V) \land (x \neq y \land P = \{x, y\})) \to \{x, y\} \in 𝒫 V$
15		eleq1	$⊢ P = \{x, y\} \to (P \in 𝒫 V \leftrightarrow \{x, y\} \in 𝒫 V)$
16	15	ad2antll	$⊢ ((x \in V \land y \in V) \land (x \neq y \land P = \{x, y\})) \to (P \in 𝒫 V \leftrightarrow \{x, y\} \in 𝒫 V)$
17	14 16	mpbird	$⊢ ((x \in V \land y \in V) \land (x \neq y \land P = \{x, y\})) \to P \in 𝒫 V$
18		fveq2	$⊢ P = \{x, y\} \to \|P\| = \|\{x, y\}\|$
19	18	ad2antll	$⊢ ((x \in V \land y \in V) \land (x \neq y \land P = \{x, y\})) \to \|P\| = \|\{x, y\}\|$
20		hashprg	$⊢ (x \in V \land y \in V) \to (x \neq y \leftrightarrow \|\{x, y\}\| = 2)$
21	20	biimpcd	$⊢ x \neq y \to ((x \in V \land y \in V) \to \|\{x, y\}\| = 2)$
22	21	adantr	$⊢ (x \neq y \land P = \{x, y\}) \to ((x \in V \land y \in V) \to \|\{x, y\}\| = 2)$
23	22	impcom	$⊢ ((x \in V \land y \in V) \land (x \neq y \land P = \{x, y\})) \to \|\{x, y\}\| = 2$
24	19 23	eqtrd	$⊢ ((x \in V \land y \in V) \land (x \neq y \land P = \{x, y\})) \to \|P\| = 2$
25	17 24	jca	$⊢ ((x \in V \land y \in V) \land (x \neq y \land P = \{x, y\})) \to (P \in 𝒫 V \land \|P\| = 2)$
26	25	ex	$⊢ (x \in V \land y \in V) \to ((x \neq y \land P = \{x, y\}) \to (P \in 𝒫 V \land \|P\| = 2))$
27	26	rexlimivv	$⊢ \exists x \in V \exists y \in V (x \neq y \land P = \{x, y\}) \to (P \in 𝒫 V \land \|P\| = 2)$
28	12 27	impbii	$⊢ (P \in 𝒫 V \land \|P\| = 2) \leftrightarrow \exists x \in V \exists y \in V (x \neq y \land P = \{x, y\})$
29	2 28	bitri	$⊢ P \in \{z \in 𝒫 V \| \|z\| = 2\} \leftrightarrow \exists x \in V \exists y \in V (x \neq y \land P = \{x, y\})$

Metamath Proof Explorer

Theorem elss2prb

Proof