Theorem suppr 4650

Description: The supremum of a pair.

Hypothesis

Ref	Expression
suppr.1	|- R Or A

Assertion

Ref	Expression
suppr	|- ((B e. A /\ C e. A) -> sup({B, C}, A, R) = if(CRB, B, C))

Proof of Theorem suppr

Step	Hyp	Ref	Expression
1		breq2 2678	. . . . . . . . . . 11 |- (y = B -> (BRy <-> BRB))
2	1	notbid 622	. . . . . . . . . 10 |- (y = B -> (-. BRy <-> -. BRB))
3		suppr.1	. . . . . . . . . . . 12 |- R Or A
4		sonr 2911	. . . . . . . . . . . 12 |- ((R Or A /\ B e. A) -> -. BRB)
5	3, 4	mpan 707	. . . . . . . . . . 11 |- (B e. A -> -. BRB)
6	5	ad2antrr 413	. . . . . . . . . 10 |- (((B e. A /\ C e. A) /\ CRB) -> -. BRB)
7	2, 6	syl5cbir 218	. . . . . . . . 9 |- (((B e. A /\ C e. A) /\ CRB) -> (y = B -> -. BRy))
8		breq2 2678	. . . . . . . . . . 11 |- (y = C -> (BRy <-> BRC))
9	8	notbid 622	. . . . . . . . . 10 |- (y = C -> (-. BRy <-> -. BRC))
10		so2nr 2914	. . . . . . . . . . . . . 14 |- ((R Or A /\ (C e. A /\ B e. A)) -> -. (CRB /\ BRC))
11	3, 10	mpan 707	. . . . . . . . . . . . 13 |- ((C e. A /\ B e. A) -> -. (CRB /\ BRC))
12		imnan 249	. . . . . . . . . . . . 13 |- ((CRB -> -. BRC) <-> -. (CRB /\ BRC))
13	11, 12	sylibr 207	. . . . . . . . . . . 12 |- ((C e. A /\ B e. A) -> (CRB -> -. BRC))
14	13	ancoms 447	. . . . . . . . . . 11 |- ((B e. A /\ C e. A) -> (CRB -> -. BRC))
15	14	imp 357	. . . . . . . . . 10 |- (((B e. A /\ C e. A) /\ CRB) -> -. BRC)
16	9, 15	syl5cbir 218	. . . . . . . . 9 |- (((B e. A /\ C e. A) /\ CRB) -> (y = C -> -. BRy))
17	7, 16	jaod 433	. . . . . . . 8 |- (((B e. A /\ C e. A) /\ CRB) -> ((y = B \/ y = C) -> -. BRy))
18		iftrue 2418	. . . . . . . . . . 11 |- (CRB -> if(CRB, B, C) = B)
19	18	breq1d 2684	. . . . . . . . . 10 |- (CRB -> (if(CRB, B, C)Ry <-> BRy))
20	19	notbid 622	. . . . . . . . 9 |- (CRB -> (-. if(CRB, B, C)Ry <-> -. BRy))
21	20	adantl 397	. . . . . . . 8 |- (((B e. A /\ C e. A) /\ CRB) -> (-. if(CRB, B, C)Ry <-> -. BRy))
22	17, 21	sylibrd 211	. . . . . . 7 |- (((B e. A /\ C e. A) /\ CRB) -> ((y = B \/ y = C) -> -. if(CRB, B, C)Ry))
23		breq2 2678	. . . . . . . . . . 11 |- (y = B -> (CRy <-> CRB))
24	23	notbid 622	. . . . . . . . . 10 |- (y = B -> (-. CRy <-> -. CRB))
25		pm3.27 330	. . . . . . . . . 10 |- (((B e. A /\ C e. A) /\ -. CRB) -> -. CRB)
26	24, 25	syl5cbir 218	. . . . . . . . 9 |- (((B e. A /\ C e. A) /\ -. CRB) -> (y = B -> -. CRy))
27		breq2 2678	. . . . . . . . . . 11 |- (y = C -> (CRy <-> CRC))
28	27	notbid 622	. . . . . . . . . 10 |- (y = C -> (-. CRy <-> -. CRC))
29		sonr 2911	. . . . . . . . . . . 12 |- ((R Or A /\ C e. A) -> -. CRC)
30	3, 29	mpan 707	. . . . . . . . . . 11 |- (C e. A -> -. CRC)
31	30	ad2antlr 414	. . . . . . . . . 10 |- (((B e. A /\ C e. A) /\ -. CRB) -> -. CRC)
32	28, 31	syl5cbir 218	. . . . . . . . 9 |- (((B e. A /\ C e. A) /\ -. CRB) -> (y = C -> -. CRy))
33	26, 32	jaod 433	. . . . . . . 8 |- (((B e. A /\ C e. A) /\ -. CRB) -> ((y = B \/ y = C) -> -. CRy))
34		iffalse 2419	. . . . . . . . . . 11 |- (-. CRB -> if(CRB, B, C) = C)
35	34	breq1d 2684	. . . . . . . . . 10 |- (-. CRB -> (if(CRB, B, C)Ry <-> CRy))
36	35	notbid 622	. . . . . . . . 9 |- (-. CRB -> (-. if(CRB, B, C)Ry <-> -. CRy))
37	36	adantl 397	. . . . . . . 8 |- (((B e. A /\ C e. A) /\ -. CRB) -> (-. if(CRB, B, C)Ry <-> -. CRy))
38	33, 37	sylibrd 211	. . . . . . 7 |- (((B e. A /\ C e. A) /\ -. CRB) -> ((y = B \/ y = C) -> -. if(CRB, B, C)Ry))
39	22, 38	pm2.61dan 488	. . . . . 6 |- ((B e. A /\ C e. A) -> ((y = B \/ y = C) -> -. if(CRB, B, C)Ry))
40		visset 1860	. . . . . . 7 |- y e. V
41	40	elpr 2476	. . . . . 6 |- (y e. {B, C} <-> (y = B \/ y = C))
42	39, 41	syl5ib 213	. . . . 5 |- ((B e. A /\ C e. A) -> (y e. {B, C} -> -. if(CRB, B, C)Ry))
43	42	r19.21aiv 1760	. . . 4 |- ((B e. A /\ C e. A) -> A.y e. {B, C} -. if(CRB, B, C)Ry)
44		breq2 2678	. . . . . . . . 9 |- (z = if(CRB, B, C) -> (yRz <-> yRif(CRB, B, C)))
45	44	rcla4ev 1924	. . . . . . . 8 |- ((if(CRB, B, C) e. {B, C} /\ yRif(CRB, B, C)) -> E.z e. {B, C}yRz)
46		ifpr 2479	. . . . . . . 8 |- ((B e. A /\ C e. A) -> if(CRB, B, C) e. {B, C})
47	45, 46	sylan 459	. . . . . . 7 |- (((B e. A /\ C e. A) /\ yRif(CRB, B, C)) -> E.z e. {B, C}yRz)
48	47	ex 380	. . . . . 6 |- ((B e. A /\ C e. A) -> (yRif(CRB, B, C) -> E.z e. {B, C}yRz))
49	48	a1d 12	. . . . 5 |- ((B e. A /\ C e. A) -> (y e. A -> (yRif(CRB, B, C) -> E.z e. {B, C}yRz)))
50	49	r19.21aiv 1760	. . . 4 |- ((B e. A /\ C e. A) -> A.y e. A (yRif(CRB, B, C) -> E.z e. {B, C}yRz))
51	43, 50	jca 295	. . 3 |- ((B e. A /\ C e. A) -> (A.y e. {B, C} -. if(CRB, B, C)Ry /\ A.y e. A (yRif(CRB, B, C) -> E.z e. {B, C}yRz)))
52		breq1 2677	. . . . . . . 8 |- (x = if(CRB, B, C) -> (xRy <-> if(CRB, B, C)Ry))
53	52	notbid 622	. . . . . . 7 |- (x = if(CRB, B, C) -> (-. xRy <-> -. if(CRB, B, C)Ry))
54	53	ralbidv 1710	. . . . . 6 |- (x = if(CRB, B, C) -> (A.y e. {B, C} -. xRy <-> A.y e. {B, C} -. if(CRB, B, C)Ry))
55		breq2 2678	. . . . . . . 8 |- (x = if(CRB, B, C) -> (yRx <-> yRif(CRB, B, C)))
56	55	imbi1d 624	. . . . . . 7 |- (x = if(CRB, B, C) -> ((yRx -> E.z e. {B, C}yRz) <-> (yRif(CRB, B, C) -> E.z e. {B, C}yRz)))
57	56	ralbidv 1710	. . . . . 6 |- (x = if(CRB, B, C) -> (A.y e. A (yRx -> E.z e. {B, C}yRz) <-> A.y e. A (yRif(CRB, B, C) -> E.z e. {B, C}yRz)))
58	54, 57	anbi12d 639	. . . . 5 |- (x = if(CRB, B, C) -> ((A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)) <-> (A.y e. {B, C} -. if(CRB, B, C)Ry /\ A.y e. A (yRif(CRB, B, C) -> E.z e. {B, C}yRz))))
59	58	reuuni2 2941	. . . 4 |- ((if(CRB, B, C) e. A /\ E!x e. A (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz))) -> ((A.y e. {B, C} -. if(CRB, B, C)Ry /\ A.y e. A (yRif(CRB, B, C) -> E.z e. {B, C}yRz)) <-> U.{x e. A | (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz))} = if(CRB, B, C)))
60		ifcl 2432	. . . 4 |- ((B e. A /\ C e. A