Theorem gelsupvalOLD 10411

Description: The greatest element of a set is the supremum. Note that the converse is not true. The supremum might not be an element of the set considered. OBSOLETE - Use supmax 4576 instead.

Hypothesis

Ref	Expression
gelsupvalOLD.1	|- R Or A

Assertion

Ref	Expression
gelsupvalOLD	|- ((C e. B /\ (C e. A /\ A.y e. B -. CRy)) -> sup(B, A, R) = C)

Distinct variable groups:   y,A   y,B   y,C   y,R

Proof of Theorem gelsupvalOLD

Step	Hyp	Ref	Expression
1		eleq1 1533	. . . . 5 |- (x = C -> (x e. B <-> C e. B))
2		eleq1 1533	. . . . . 6 |- (x = C -> (x e. A <-> C e. A))
3		breq1 2619	. . . . . . . 8 |- (x = C -> (xRy <-> CRy))
4	3	negbid 610	. . . . . . 7 |- (x = C -> (-. xRy <-> -. CRy))
5	4	ralbidv 1662	. . . . . 6 |- (x = C -> (A.y e. B -. xRy <-> A.y e. B -. CRy))
6	2, 5	anbi12d 627	. . . . 5 |- (x = C -> ((x e. A /\ A.y e. B -. xRy) <-> (C e. A /\ A.y e. B -. CRy)))
7	1, 6	anbi12d 627	. . . 4 |- (x = C -> ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) <-> (C e. B /\ (C e. A /\ A.y e. B -. CRy))))
8		eqeq2 1483	. . . 4 |- (x = C -> (sup(B, A, R) = x <-> sup(B, A, R) = C))
9	7, 8	imbi12d 625	. . 3 |- (x = C -> (((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> sup(B, A, R) = x) <-> ((C e. B /\ (C e. A /\ A.y e. B -. CRy)) -> sup(B, A, R) = C)))
10		gelcomplOLD 10410	. . . . . . . . 9 |- ((x e. A /\ (A.y e. B -. xRy /\ x e. B)) -> E.x e. A (A.z e. B -. xRz /\ A.z e. A (zRx -> E.y e. B zRy)))
11	10	ancom2s 487	. . . . . . . 8 |- ((x e. A /\ (x e. B /\ A.y e. B -. xRy)) -> E.x e. A (A.z e. B -. xRz /\ A.z e. A (zRx -> E.y e. B zRy)))
12	11	an1s 486	. . . . . . 7 |- ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> E.x e. A (A.z e. B -. xRz /\ A.z e. A (zRx -> E.y e. B zRy)))
13		gelsupvalOLD.1	. . . . . . . 8 |- R Or A
14	13	supub 4567	. . . . . . 7 |- (E.x e. A (A.z e. B -. xRz /\ A.z e. A (zRx -> E.y e. B zRy)) -> (x e. B -> -. sup(B, A, R)Rx))
15	12, 14	syl 10	. . . . . 6 |- ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> (x e. B -> -. sup(B, A, R)Rx))
16	13	supnub 4569	. . . . . . 7 |- (E.x e. A (A.z e. B -. xRz /\ A.z e. A (zRx -> E.y e. B zRy)) -> ((x e. A /\ A.y e. B -. xRy) -> -. xRsup(B, A, R)))
17	12, 16	syl 10	. . . . . 6 |- ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> ((x e. A /\ A.y e. B -. xRy) -> -. xRsup(B, A, R)))
18	15, 17	anim12d 557	. . . . 5 |- ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> (-. sup(B, A, R)Rx /\ -. xRsup(B, A, R))))
19	18	pm2.43i 64	. . . 4 |- ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> (-. sup(B, A, R)Rx /\ -. xRsup(B, A, R)))
20		sotrieq2 2859	. . . . . 6 |- ((R Or A /\ (sup(B, A, R) e. A /\ x e. A)) -> (sup(B, A, R) = x <-> (-. sup(B, A, R)Rx /\ -. xRsup(B, A, R))))
21	13, 20	mpan 694	. . . . 5 |- ((sup(B, A, R) e. A /\ x e. A) -> (sup(B, A, R) = x <-> (-. sup(B, A, R)Rx /\ -. xRsup(B, A, R))))
22	13	supcl 4566	. . . . . 6 |- (E.x e. A (A.z e. B -. xRz /\ A.z e. A (zRx -> E.y e. B zRy)) -> sup(B, A, R) e. A)
23	12, 22	syl 10	. . . . 5 |- ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> sup(B, A, R) e. A)
24		simprl 414	. . . . 5 |- ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> x e. A)
25	21, 23, 24	sylanc 471	. . . 4 |- ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> (sup(B, A, R) = x <-> (-. sup(B, A, R)Rx /\ -. xRsup(B, A, R))))
26	19, 25	mpbird 196	. . 3 |- ((x e. B /\ (x e. A /\ A.y e. B -. xRy)) -> sup(B, A, R) = x)
27	9, 26	vtoclg 1845	. 2 |- (C e. B -> ((C e. B /\ (C e. A /\ A.y e. B -. CRy)) -> sup(B, A, R) = C))
28	27	anabsi5 495	1 |- ((C e. B /\ (C e. A /\ A.y e. B -. CRy)) -> sup(B, A, R) = C)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   = wceq 955   e. wcel 957  A.wral 1644  E.wrex 1645   class class class wbr 2616   Or wor 2836  supcsup 4560

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2700  ax-pow 2739  ax-un 2863

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-reu 1650  df-rab 1651  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-pw 2400  df-sn 2410  df-pr 2411  df-op 2414  df-uni 2501  df-br 2617  df-po 2837  df-so 2847  df-sup 4561

Copyright terms: Public domain