Theorem suppr 5680

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		ifcl 3007	. . . 4 |- ((B e. A /\ C e. A) -> if(CRB, B, C) e. A)
2		breq2 3342	. . . . . . . . . . . . . 14 |- (y = B -> (BRy <-> BRB))
3	2	notbid 673	. . . . . . . . . . . . 13 |- (y = B -> (-. BRy <-> -. BRB))
4		suppr.1	. . . . . . . . . . . . . . 15 |- R Or A
5		sonr 3610	. . . . . . . . . . . . . . 15 |- ((R Or A /\ B e. A) -> -. BRB)
6	4, 5	mpan 759	. . . . . . . . . . . . . 14 |- (B e. A -> -. BRB)
7	6	ad2antrr 440	. . . . . . . . . . . . 13 |- (((B e. A /\ C e. A) /\ CRB) -> -. BRB)
8	3, 7	syl5cbir 228	. . . . . . . . . . . 12 |- (((B e. A /\ C e. A) /\ CRB) -> (y = B -> -. BRy))
9		breq2 3342	. . . . . . . . . . . . . 14 |- (y = C -> (BRy <-> BRC))
10	9	notbid 673	. . . . . . . . . . . . 13 |- (y = C -> (-. BRy <-> -. BRC))
11		so2nr 3613	. . . . . . . . . . . . . . . . 17 |- ((R Or A /\ (C e. A /\ B e. A)) -> -. (CRB /\ BRC))
12	4, 11	mpan 759	. . . . . . . . . . . . . . . 16 |- ((C e. A /\ B e. A) -> -. (CRB /\ BRC))
13		imnan 261	. . . . . . . . . . . . . . . 16 |- ((CRB -> -. BRC) <-> -. (CRB /\ BRC))
14	12, 13	sylibr 217	. . . . . . . . . . . . . . 15 |- ((C e. A /\ B e. A) -> (CRB -> -. BRC))
15	14	ancoms 484	. . . . . . . . . . . . . 14 |- ((B e. A /\ C e. A) -> (CRB -> -. BRC))
16	15	imp 377	. . . . . . . . . . . . 13 |- (((B e. A /\ C e. A) /\ CRB) -> -. BRC)
17	10, 16	syl5cbir 228	. . . . . . . . . . . 12 |- (((B e. A /\ C e. A) /\ CRB) -> (y = C -> -. BRy))
18	8, 17	jaod 469	. . . . . . . . . . 11 |- (((B e. A /\ C e. A) /\ CRB) -> ((y = B \/ y = C) -> -. BRy))
19		iftrue 2989	. . . . . . . . . . . . . 14 |- (CRB -> if(CRB, B, C) = B)
20	19	breq1d 3348	. . . . . . . . . . . . 13 |- (CRB -> (if(CRB, B, C)Ry <-> BRy))
21	20	notbid 673	. . . . . . . . . . . 12 |- (CRB -> (-. if(CRB, B, C)Ry <-> -. BRy))
22	21	adantl 424	. . . . . . . . . . 11 |- (((B e. A /\ C e. A) /\ CRB) -> (-. if(CRB, B, C)Ry <-> -. BRy))
23	18, 22	sylibrd 221	. . . . . . . . . 10 |- (((B e. A /\ C e. A) /\ CRB) -> ((y = B \/ y = C) -> -. if(CRB, B, C)Ry))
24		breq2 3342	. . . . . . . . . . . . . 14 |- (y = B -> (CRy <-> CRB))
25	24	notbid 673	. . . . . . . . . . . . 13 |- (y = B -> (-. CRy <-> -. CRB))
26		simpr 350	. . . . . . . . . . . . 13 |- (((B e. A /\ C e. A) /\ -. CRB) -> -. CRB)
27	25, 26	syl5cbir 228	. . . . . . . . . . . 12 |- (((B e. A /\ C e. A) /\ -. CRB) -> (y = B -> -. CRy))
28		breq2 3342	. . . . . . . . . . . . . 14 |- (y = C -> (CRy <-> CRC))
29	28	notbid 673	. . . . . . . . . . . . 13 |- (y = C -> (-. CRy <-> -. CRC))
30		sonr 3610	. . . . . . . . . . . . . . 15 |- ((R Or A /\ C e. A) -> -. CRC)
31	4, 30	mpan 759	. . . . . . . . . . . . . 14 |- (C e. A -> -. CRC)
32	31	ad2antlr 441	. . . . . . . . . . . . 13 |- (((B e. A /\ C e. A) /\ -. CRB) -> -. CRC)
33	29, 32	syl5cbir 228	. . . . . . . . . . . 12 |- (((B e. A /\ C e. A) /\ -. CRB) -> (y = C -> -. CRy))
34	27, 33	jaod 469	. . . . . . . . . . 11 |- (((B e. A /\ C e. A) /\ -. CRB) -> ((y = B \/ y = C) -> -. CRy))
35		iffalse 2991	. . . . . . . . . . . . . 14 |- (-. CRB -> if(CRB, B, C) = C)
36	35	breq1d 3348	. . . . . . . . . . . . 13 |- (-. CRB -> (if(CRB, B, C)Ry <-> CRy))
37	36	notbid 673	. . . . . . . . . . . 12 |- (-. CRB -> (-. if(CRB, B, C)Ry <-> -. CRy))
38	37	adantl 424	. . . . . . . . . . 11 |- (((B e. A /\ C e. A) /\ -. CRB) -> (-. if(CRB, B, C)Ry <-> -. CRy))
39	34, 38	sylibrd 221	. . . . . . . . . 10 |- (((B e. A /\ C e. A) /\ -. CRB) -> ((y = B \/ y = C) -> -. if(CRB, B, C)Ry))
40	23, 39	pm2.61dan 535	. . . . . . . . 9 |- ((B e. A /\ C e. A) -> ((y = B \/ y = C) -> -. if(CRB, B, C)Ry))
41		visset 2295	. . . . . . . . . 10 |- y e. _V
42	41	elpr 3061	. . . . . . . . 9 |- (y e. {B, C} <-> (y = B \/ y = C))
43	40, 42	syl5ib 223	. . . . . . . 8 |- ((B e. A /\ C e. A) -> (y e. {B, C} -> -. if(CRB, B, C)Ry))
44	43	r19.21aiv 2175	. . . . . . 7 |- ((B e. A /\ C e. A) -> A.y e. {B, C} -. if(CRB, B, C)Ry)
45		breq2 3342	. . . . . . . . . . . 12 |- (z = if(CRB, B, C) -> (yRz <-> yRif(CRB, B, C)))
46	45	rcla4ev 2381	. . . . . . . . . . 11 |- ((if(CRB, B, C) e. {B, C} /\ yRif(CRB, B, C)) -> E.z e. {B, C}yRz)
47		ifpr 3077	. . . . . . . . . . 11 |- ((B e. A /\ C e. A) -> if(CRB, B, C) e. {B, C})
48	46, 47	sylan 497	. . . . . . . . . 10 |- (((B e. A /\ C e. A) /\ yRif(CRB, B, C)) -> E.z e. {B, C}yRz)
49	48	ex 402	. . . . . . . . 9 |- ((B e. A /\ C e. A) -> (yRif(CRB, B, C) -> E.z e. {B, C}yRz))
50	49	a1d 15	. . . . . . . 8 |- ((B e. A /\ C e. A) -> (y e. A -> (yRif(CRB, B, C) -> E.z e. {B, C}yRz)))
51	50	r19.21aiv 2175	. . . . . . 7 |- ((B e. A /\ C e. A) -> A.y e. A (yRif(CRB, B, C) -> E.z e. {B, C}yRz))
52		breq1 3341	. . . . . . . . . . 11 |- (x = if(CRB, B, C) -> (xRy <-> if(CRB, B, C)Ry))
53	52	notbid 673	. . . . . . . . . 10 |- (x = if(CRB, B, C) -> (-. xRy <-> -. if(CRB, B, C)Ry))
54	53	ralbidv 2123	. . . . . . . . 9 |- (x = if(CRB, B, C) -> (A.y e. {B, C} -. xRy <-> A.y e. {B, C} -. if(CRB, B, C)Ry))
55		breq2 3342	. . . . . . . . . . 11 |- (x = if(CRB, B, C) -> (yRx <-> yRif(CRB, B, C)))
56	55	imbi1d 675	. . . . . . . . . 10 |- (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 2123	. . . . . . . . 9 |- (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 690	. . . . . . . 8 |- (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	rcla4ev 2381	. . . . . . 7 |- ((if(CRB, B, 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))) -> E.x e. A (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)))
60	1, 44, 51, 59	syl12anc 1098	. . . . . 6 |- ((B e. A /\ C e. A) -> E.x e. A (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)))
61	4	supmo 5666	. . . . . 6 |- E*x(x e. A /\ (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)))
62	60, 61	jctir 317	. . . . 5 |- ((B e. A /\ C e. A) -> (E.x e. A (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)) /\ E*x(x e. A /\ (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)))))
63		reu5 2441	. . . . 5 |- (E!x e. A (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)) <-> (E.x e. A (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)) /\ E*x(x e. A /\ (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)))))
64	62, 63	sylibr 217	. . . 4 |- ((B e. A /\ C e. A) -> E!x e. A (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz)))
65	58	reuuni2 3811	. . . 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)))
66	1, 64, 65	syl11anc 524	. . 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)) <-> 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)))
67	66, 44, 51	mpbi2and 801	. 2 |- ((B e. A /\ C e. A) -> 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))
68		df-sup 5664	. 2 |- sup({B, C}, A, R) = U.{x e. A | (A.y e. {B, C} -. xRy /\ A.y e. A (yRx -> E.z e. {B, C}yRz))}
69	67, 68	syl5eq 1940	1 |- ((B e. A /\ C e. A) -> sup({B, C}, A, R) = if(CRB, B, C))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300  E*wmo 1772  A.wral 2105  E.wrex 2106  E!wreu 2107  {crab 2108  ifcif 2982  {cpr 3045  U.cuni 3177   class class class wbr 3338   Or wor 3590  supcsup 5663

This theorem is referenced by:  supsn 5681  metxpdval 9106

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-po 3591  df-so 3604  df-sup 5664

Copyright terms: Public domain