prproropf1olem3

	Ref	Expression
Hypotheses	prproropf1o.o	$⊢ O = R \cap (V \times V)$
	prproropf1o.p	$⊢ P = \{p \in 𝒫 V \| \|p\| = 2\}$
	prproropf1o.f	$⊢ F = (p \in P ⟼ ⟨inf (p, V, R), sup (p, V, R)⟩)$
Assertion	prproropf1olem3	$⊢ (R Or V \land W \in O) \to F (\{1^{st} (W), 2^{nd} (W)\}) = ⟨1^{st} (W), 2^{nd} (W)⟩$

Proof

Step	Hyp	Ref	Expression
1		prproropf1o.o	$⊢ O = R \cap (V \times V)$
2		prproropf1o.p	$⊢ P = \{p \in 𝒫 V \| \|p\| = 2\}$
3		prproropf1o.f	$⊢ F = (p \in P ⟼ ⟨inf (p, V, R), sup (p, V, R)⟩)$
4		infeq1	$⊢ p = \{1^{st} (W), 2^{nd} (W)\} \to inf (p, V, R) = inf (\{1^{st} (W), 2^{nd} (W)\}, V, R)$
5		supeq1	$⊢ p = \{1^{st} (W), 2^{nd} (W)\} \to sup (p, V, R) = sup (\{1^{st} (W), 2^{nd} (W)\}, V, R)$
6	4 5	opeq12d	$⊢ p = \{1^{st} (W), 2^{nd} (W)\} \to ⟨inf (p, V, R), sup (p, V, R)⟩ = ⟨inf (\{1^{st} (W), 2^{nd} (W)\}, V, R), sup (\{1^{st} (W), 2^{nd} (W)\}, V, R)⟩$
7	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))$
8		simpl	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to R Or V$
9		simprll	$⊢ (R Or 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) \in V$
10		simprlr	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to 2^{nd} (W) \in V$
11		infpr	$⊢ (R Or V \land 1^{st} (W) \in V \land 2^{nd} (W) \in V) \to inf (\{1^{st} (W), 2^{nd} (W)\}, V, R) = if (1^{st} (W) R 2^{nd} (W), 1^{st} (W), 2^{nd} (W))$
12	8 9 10 11	syl3anc	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to inf (\{1^{st} (W), 2^{nd} (W)\}, V, R) = if (1^{st} (W) R 2^{nd} (W), 1^{st} (W), 2^{nd} (W))$
13		iftrue	$⊢ 1^{st} (W) R 2^{nd} (W) \to if (1^{st} (W) R 2^{nd} (W), 1^{st} (W), 2^{nd} (W)) = 1^{st} (W)$
14	13	ad2antll	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to if (1^{st} (W) R 2^{nd} (W), 1^{st} (W), 2^{nd} (W)) = 1^{st} (W)$
15	12 14	eqtrd	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to inf (\{1^{st} (W), 2^{nd} (W)\}, V, R) = 1^{st} (W)$
16		suppr	$⊢ (R Or V \land 1^{st} (W) \in V \land 2^{nd} (W) \in V) \to sup (\{1^{st} (W), 2^{nd} (W)\}, V, R) = if (2^{nd} (W) R 1^{st} (W), 1^{st} (W), 2^{nd} (W))$
17	8 9 10 16	syl3anc	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to sup (\{1^{st} (W), 2^{nd} (W)\}, V, R) = if (2^{nd} (W) R 1^{st} (W), 1^{st} (W), 2^{nd} (W))$
18		soasym	$⊢ (R Or V \land (1^{st} (W) \in V \land 2^{nd} (W) \in V)) \to (1^{st} (W) R 2^{nd} (W) \to \neg 2^{nd} (W) R 1^{st} (W))$
19	18	impr	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to \neg 2^{nd} (W) R 1^{st} (W)$
20	19	iffalsed	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to if (2^{nd} (W) R 1^{st} (W), 1^{st} (W), 2^{nd} (W)) = 2^{nd} (W)$
21	17 20	eqtrd	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to sup (\{1^{st} (W), 2^{nd} (W)\}, V, R) = 2^{nd} (W)$
22	15 21	opeq12d	$⊢ (R Or V \land ((1^{st} (W) \in V \land 2^{nd} (W) \in V) \land 1^{st} (W) R 2^{nd} (W))) \to ⟨inf (\{1^{st} (W), 2^{nd} (W)\}, V, R), sup (\{1^{st} (W), 2^{nd} (W)\}, V, R)⟩ = ⟨1^{st} (W), 2^{nd} (W)⟩$
23	22	3adantr1	$⊢ (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 ⟨inf (\{1^{st} (W), 2^{nd} (W)\}, V, R), sup (\{1^{st} (W), 2^{nd} (W)\}, V, R)⟩ = ⟨1^{st} (W), 2^{nd} (W)⟩$
24	7 23	sylan2b	$⊢ (R Or V \land W \in O) \to ⟨inf (\{1^{st} (W), 2^{nd} (W)\}, V, R), sup (\{1^{st} (W), 2^{nd} (W)\}, V, R)⟩ = ⟨1^{st} (W), 2^{nd} (W)⟩$
25	6 24	sylan9eqr	$⊢ ((R Or V \land W \in O) \land p = \{1^{st} (W), 2^{nd} (W)\}) \to ⟨inf (p, V, R), sup (p, V, R)⟩ = ⟨1^{st} (W), 2^{nd} (W)⟩$
26	1 2	prproropf1olem1	$⊢ (R Or V \land W \in O) \to \{1^{st} (W), 2^{nd} (W)\} \in P$
27		opex	$⊢ ⟨1^{st} (W), 2^{nd} (W)⟩ \in V$
28	27	a1i	$⊢ (R Or V \land W \in O) \to ⟨1^{st} (W), 2^{nd} (W)⟩ \in V$
29	3 25 26 28	fvmptd2	$⊢ (R Or V \land W \in O) \to F (\{1^{st} (W), 2^{nd} (W)\}) = ⟨1^{st} (W), 2^{nd} (W)⟩$

Metamath Proof Explorer

Theorem prproropf1olem3

Proof