pr2cv

Description: If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023)

		Ref	Expression
	Assertion	pr2cv	$⊢ \{A, B\} \approx 2_{𝑜} \to (A \in V \land B \in V)$

Proof

Step	Hyp	Ref	Expression
1		en2	$⊢ \{A, B\} \approx 2_{𝑜} \to \exists x \exists y \{A, B\} = \{x, y\}$
2		breq1	$⊢ \{A, B\} = \{x, y\} \to (\{A, B\} \approx 2_{𝑜} \leftrightarrow \{x, y\} \approx 2_{𝑜})$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5		pr2ne	$⊢ (x \in V \land y \in V) \to (\{x, y\} \approx 2_{𝑜} \leftrightarrow x \neq y)$
6	5	el2v	$⊢ \{x, y\} \approx 2_{𝑜} \leftrightarrow x \neq y$
7	6	biimpi	$⊢ \{x, y\} \approx 2_{𝑜} \to x \neq y$
8		preq12nebg	$⊢ (x \in V \land y \in V \land x \neq y) \to (\{x, y\} = \{A, B\} \leftrightarrow ((x = A \land y = B) \lor (x = B \land y = A)))$
9		eqvisset	$⊢ x = A \to A \in V$
10		eqvisset	$⊢ y = B \to B \in V$
11	9 10	anim12i	$⊢ (x = A \land y = B) \to (A \in V \land B \in V)$
12		eqvisset	$⊢ x = B \to B \in V$
13		eqvisset	$⊢ y = A \to A \in V$
14	12 13	anim12ci	$⊢ (x = B \land y = A) \to (A \in V \land B \in V)$
15	11 14	jaoi	$⊢ ((x = A \land y = B) \lor (x = B \land y = A)) \to (A \in V \land B \in V)$
16	8 15	syl6bi	$⊢ (x \in V \land y \in V \land x \neq y) \to (\{x, y\} = \{A, B\} \to (A \in V \land B \in V))$
17	3 4 7 16	mp3an12i	$⊢ \{x, y\} \approx 2_{𝑜} \to (\{x, y\} = \{A, B\} \to (A \in V \land B \in V))$
18	17	com12	$⊢ \{x, y\} = \{A, B\} \to (\{x, y\} \approx 2_{𝑜} \to (A \in V \land B \in V))$
19	18	eqcoms	$⊢ \{A, B\} = \{x, y\} \to (\{x, y\} \approx 2_{𝑜} \to (A \in V \land B \in V))$
20	2 19	sylbid	$⊢ \{A, B\} = \{x, y\} \to (\{A, B\} \approx 2_{𝑜} \to (A \in V \land B \in V))$
21	20	exlimivv	$⊢ \exists x \exists y \{A, B\} = \{x, y\} \to (\{A, B\} \approx 2_{𝑜} \to (A \in V \land B \in V))$
22	1 21	mpcom	$⊢ \{A, B\} \approx 2_{𝑜} \to (A \in V \land B \in V)$

Metamath Proof Explorer

Theorem pr2cv

Proof