Metamath Proof Explorer


Theorem supmo

Description: Any class B has at most one supremum in A (where R is interpreted as 'less than'). (Contributed by NM, 5-May-1999) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis supmo.1 φROrA
Assertion supmo φ*xAyB¬xRyyAyRxzByRz

Proof

Step Hyp Ref Expression
1 supmo.1 φROrA
2 ancom yB¬xRyyB¬wRyyB¬wRyyB¬xRy
3 2 anbi2ci yB¬xRyyB¬wRyyAyRwzByRzyAyRxzByRzyAyRwzByRzyAyRxzByRzyB¬wRyyB¬xRy
4 an42 yB¬xRyyAyRxzByRzyB¬wRyyAyRwzByRzyB¬xRyyB¬wRyyAyRwzByRzyAyRxzByRz
5 an42 yAyRwzByRzyB¬xRyyAyRxzByRzyB¬wRyyAyRwzByRzyAyRxzByRzyB¬wRyyB¬xRy
6 3 4 5 3bitr4i yB¬xRyyAyRxzByRzyB¬wRyyAyRwzByRzyAyRwzByRzyB¬xRyyAyRxzByRzyB¬wRy
7 ralnex yB¬xRy¬yBxRy
8 breq1 y=xyRwxRw
9 breq1 y=xyRzxRz
10 9 rexbidv y=xzByRzzBxRz
11 8 10 imbi12d y=xyRwzByRzxRwzBxRz
12 11 rspcva xAyAyRwzByRzxRwzBxRz
13 breq2 y=zxRyxRz
14 13 cbvrexvw yBxRyzBxRz
15 12 14 syl6ibr xAyAyRwzByRzxRwyBxRy
16 15 con3d xAyAyRwzByRz¬yBxRy¬xRw
17 7 16 syl5bi xAyAyRwzByRzyB¬xRy¬xRw
18 17 expimpd xAyAyRwzByRzyB¬xRy¬xRw
19 18 ad2antrl ROrAxAwAyAyRwzByRzyB¬xRy¬xRw
20 ralnex yB¬wRy¬yBwRy
21 breq1 y=wyRxwRx
22 breq1 y=wyRzwRz
23 22 rexbidv y=wzByRzzBwRz
24 21 23 imbi12d y=wyRxzByRzwRxzBwRz
25 24 rspcva wAyAyRxzByRzwRxzBwRz
26 breq2 y=zwRywRz
27 26 cbvrexvw yBwRyzBwRz
28 25 27 syl6ibr wAyAyRxzByRzwRxyBwRy
29 28 con3d wAyAyRxzByRz¬yBwRy¬wRx
30 20 29 syl5bi wAyAyRxzByRzyB¬wRy¬wRx
31 30 expimpd wAyAyRxzByRzyB¬wRy¬wRx
32 31 ad2antll ROrAxAwAyAyRxzByRzyB¬wRy¬wRx
33 19 32 anim12d ROrAxAwAyAyRwzByRzyB¬xRyyAyRxzByRzyB¬wRy¬xRw¬wRx
34 6 33 syl5bi ROrAxAwAyB¬xRyyAyRxzByRzyB¬wRyyAyRwzByRz¬xRw¬wRx
35 sotrieq2 ROrAxAwAx=w¬xRw¬wRx
36 34 35 sylibrd ROrAxAwAyB¬xRyyAyRxzByRzyB¬wRyyAyRwzByRzx=w
37 36 ralrimivva ROrAxAwAyB¬xRyyAyRxzByRzyB¬wRyyAyRwzByRzx=w
38 1 37 syl φxAwAyB¬xRyyAyRxzByRzyB¬wRyyAyRwzByRzx=w
39 breq1 x=wxRywRy
40 39 notbid x=w¬xRy¬wRy
41 40 ralbidv x=wyB¬xRyyB¬wRy
42 breq2 x=wyRxyRw
43 42 imbi1d x=wyRxzByRzyRwzByRz
44 43 ralbidv x=wyAyRxzByRzyAyRwzByRz
45 41 44 anbi12d x=wyB¬xRyyAyRxzByRzyB¬wRyyAyRwzByRz
46 45 rmo4 *xAyB¬xRyyAyRxzByRzxAwAyB¬xRyyAyRxzByRzyB¬wRyyAyRwzByRzx=w
47 38 46 sylibr φ*xAyB¬xRyyAyRxzByRz