prproropf1olem1

	Ref	Expression
Hypotheses	prproropf1o.o	$⊢ O = R \cap (V \times V)$
	prproropf1o.p	$⊢ P = \{p \in 𝒫 V \| \|p\| = 2\}$
Assertion	prproropf1olem1	$⊢ (R Or V \land W \in O) \to \{1^{st} (W), 2^{nd} (W)\} \in P$

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	$⊢ O = R \cap (V \times V)$
2		prproropf1o.p	$⊢ P = \{p \in 𝒫 V \| \|p\| = 2\}$
3	1	prproropf1olem0	$⊢ W \in O \leftrightarrow (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))$
4		simpr2	$⊢ (R Or V \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to (1^{st} (W) \in V \land 2^{nd} (W) \in V)$
5		prelpwi	$⊢ (1^{st} (W) \in V \land 2^{nd} (W) \in V) \to \{1^{st} (W), 2^{nd} (W)\} \in 𝒫 V$
6	4 5	syl	$⊢ (R Or V \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to \{1^{st} (W), 2^{nd} (W)\} \in 𝒫 V$
7		sopo	$⊢ R Or V \to R Po V$
8	7	adantr	$⊢ (R Or V \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to R Po V$
9		simpr3	$⊢ (R Or V \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to 1^{st} (W) R 2^{nd} (W)$
10		po2ne	$⊢ (R Po V \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W)) \to 1^{st} (W) \neq 2^{nd} (W)$
11	8 4 9 10	syl3anc	$⊢ (R Or V \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to 1^{st} (W) \neq 2^{nd} (W)$
12		fvex	$⊢ 1^{st} (W) \in V$
13		fvex	$⊢ 2^{nd} (W) \in V$
14		hashprg	$⊢ (1^{st} (W) \in V \land 2^{nd} (W) \in V) \to (1^{st} (W) \neq 2^{nd} (W) \leftrightarrow \|\{1^{st} (W), 2^{nd} (W)\}\| = 2)$
15	12 13 14	mp2an	$⊢ 1^{st} (W) \neq 2^{nd} (W) \leftrightarrow \|\{1^{st} (W), 2^{nd} (W)\}\| = 2$
16	11 15	sylib	$⊢ (R Or V \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to \|\{1^{st} (W), 2^{nd} (W)\}\| = 2$
17	6 16	jca	$⊢ (R Or V \land (W = ⟨1^{st} (W), 2^{nd} (W)⟩ \land (1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to (\{1^{st} (W), 2^{nd} (W)\} \in 𝒫 V \land \|\{1^{st} (W), 2^{nd} (W)\}\| = 2)$
18	3 17	sylan2b	$⊢ (R Or V \land W \in O) \to (\{1^{st} (W), 2^{nd} (W)\} \in 𝒫 V \land \|\{1^{st} (W), 2^{nd} (W)\}\| = 2)$
19		fveqeq2	$⊢ p = \{1^{st} (W), 2^{nd} (W)\} \to (\|p\| = 2 \leftrightarrow \|\{1^{st} (W), 2^{nd} (W)\}\| = 2)$
20	19 2	elrab2	$⊢ \{1^{st} (W), 2^{nd} (W)\} \in P \leftrightarrow (\{1^{st} (W), 2^{nd} (W)\} \in 𝒫 V \land \|\{1^{st} (W), 2^{nd} (W)\}\| = 2)$
21	18 20	sylibr	$⊢ (R Or V \land W \in O) \to \{1^{st} (W), 2^{nd} (W)\} \in P$

Metamath Proof Explorer

Theorem prproropf1olem1

Proof