suppr

Description: The supremum of a pair. (Contributed by NM, 17-Jun-2007) (Proof shortened by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Assertion	suppr	$⊢ (R Or A \land B \in A \land C \in A) \to sup (\{B, C\}, A, R) = if (C R B, B, C)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (R Or A \land B \in A \land C \in A) \to R Or A$
2		ifcl	$⊢ (B \in A \land C \in A) \to if (C R B, B, C) \in A$
3	2	3adant1	$⊢ (R Or A \land B \in A \land C \in A) \to if (C R B, B, C) \in A$
4		ifpr	$⊢ (B \in A \land C \in A) \to if (C R B, B, C) \in \{B, C\}$
5	4	3adant1	$⊢ (R Or A \land B \in A \land C \in A) \to if (C R B, B, C) \in \{B, C\}$
6		breq1	$⊢ B = if (C R B, B, C) \to (B R B \leftrightarrow if (C R B, B, C) R B)$
7	6	notbid	$⊢ B = if (C R B, B, C) \to (\neg B R B \leftrightarrow \neg if (C R B, B, C) R B)$
8		breq1	$⊢ C = if (C R B, B, C) \to (C R B \leftrightarrow if (C R B, B, C) R B)$
9	8	notbid	$⊢ C = if (C R B, B, C) \to (\neg C R B \leftrightarrow \neg if (C R B, B, C) R B)$
10		sonr	$⊢ (R Or A \land B \in A) \to \neg B R B$
11	10	3adant3	$⊢ (R Or A \land B \in A \land C \in A) \to \neg B R B$
12	11	adantr	$⊢ ((R Or A \land B \in A \land C \in A) \land C R B) \to \neg B R B$
13		simpr	$⊢ ((R Or A \land B \in A \land C \in A) \land \neg C R B) \to \neg C R B$
14	7 9 12 13	ifbothda	$⊢ (R Or A \land B \in A \land C \in A) \to \neg if (C R B, B, C) R B$
15		breq1	$⊢ B = if (C R B, B, C) \to (B R C \leftrightarrow if (C R B, B, C) R C)$
16	15	notbid	$⊢ B = if (C R B, B, C) \to (\neg B R C \leftrightarrow \neg if (C R B, B, C) R C)$
17		breq1	$⊢ C = if (C R B, B, C) \to (C R C \leftrightarrow if (C R B, B, C) R C)$
18	17	notbid	$⊢ C = if (C R B, B, C) \to (\neg C R C \leftrightarrow \neg if (C R B, B, C) R C)$
19		so2nr	$⊢ (R Or A \land (C \in A \land B \in A)) \to \neg (C R B \land B R C)$
20	19	3impb	$⊢ (R Or A \land C \in A \land B \in A) \to \neg (C R B \land B R C)$
21	20	3com23	$⊢ (R Or A \land B \in A \land C \in A) \to \neg (C R B \land B R C)$
22		imnan	$⊢ (C R B \to \neg B R C) \leftrightarrow \neg (C R B \land B R C)$
23	21 22	sylibr	$⊢ (R Or A \land B \in A \land C \in A) \to (C R B \to \neg B R C)$
24	23	imp	$⊢ ((R Or A \land B \in A \land C \in A) \land C R B) \to \neg B R C$
25		sonr	$⊢ (R Or A \land C \in A) \to \neg C R C$
26	25	3adant2	$⊢ (R Or A \land B \in A \land C \in A) \to \neg C R C$
27	26	adantr	$⊢ ((R Or A \land B \in A \land C \in A) \land \neg C R B) \to \neg C R C$
28	16 18 24 27	ifbothda	$⊢ (R Or A \land B \in A \land C \in A) \to \neg if (C R B, B, C) R C$
29		breq2	$⊢ y = B \to (if (C R B, B, C) R y \leftrightarrow if (C R B, B, C) R B)$
30	29	notbid	$⊢ y = B \to (\neg if (C R B, B, C) R y \leftrightarrow \neg if (C R B, B, C) R B)$
31		breq2	$⊢ y = C \to (if (C R B, B, C) R y \leftrightarrow if (C R B, B, C) R C)$
32	31	notbid	$⊢ y = C \to (\neg if (C R B, B, C) R y \leftrightarrow \neg if (C R B, B, C) R C)$
33	30 32	ralprg	$⊢ (B \in A \land C \in A) \to (\forall y \in \{B, C\} \neg if (C R B, B, C) R y \leftrightarrow (\neg if (C R B, B, C) R B \land \neg if (C R B, B, C) R C))$
34	33	3adant1	$⊢ (R Or A \land B \in A \land C \in A) \to (\forall y \in \{B, C\} \neg if (C R B, B, C) R y \leftrightarrow (\neg if (C R B, B, C) R B \land \neg if (C R B, B, C) R C))$
35	14 28 34	mpbir2and	$⊢ (R Or A \land B \in A \land C \in A) \to \forall y \in \{B, C\} \neg if (C R B, B, C) R y$
36	35	r19.21bi	$⊢ ((R Or A \land B \in A \land C \in A) \land y \in \{B, C\}) \to \neg if (C R B, B, C) R y$
37	1 3 5 36	supmax	$⊢ (R Or A \land B \in A \land C \in A) \to sup (\{B, C\}, A, R) = if (C R B, B, C)$

Metamath Proof Explorer

Theorem suppr

Proof