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 | |
|
Assertion | supmo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | supmo.1 | |
|
2 | ancom | |
|
3 | 2 | anbi2ci | |
4 | an42 | |
|
5 | an42 | |
|
6 | 3 4 5 | 3bitr4i | |
7 | ralnex | |
|
8 | breq1 | |
|
9 | breq1 | |
|
10 | 9 | rexbidv | |
11 | 8 10 | imbi12d | |
12 | 11 | rspcva | |
13 | breq2 | |
|
14 | 13 | cbvrexvw | |
15 | 12 14 | syl6ibr | |
16 | 15 | con3d | |
17 | 7 16 | syl5bi | |
18 | 17 | expimpd | |
19 | 18 | ad2antrl | |
20 | ralnex | |
|
21 | breq1 | |
|
22 | breq1 | |
|
23 | 22 | rexbidv | |
24 | 21 23 | imbi12d | |
25 | 24 | rspcva | |
26 | breq2 | |
|
27 | 26 | cbvrexvw | |
28 | 25 27 | syl6ibr | |
29 | 28 | con3d | |
30 | 20 29 | syl5bi | |
31 | 30 | expimpd | |
32 | 31 | ad2antll | |
33 | 19 32 | anim12d | |
34 | 6 33 | syl5bi | |
35 | sotrieq2 | |
|
36 | 34 35 | sylibrd | |
37 | 36 | ralrimivva | |
38 | 1 37 | syl | |
39 | breq1 | |
|
40 | 39 | notbid | |
41 | 40 | ralbidv | |
42 | breq2 | |
|
43 | 42 | imbi1d | |
44 | 43 | ralbidv | |
45 | 41 44 | anbi12d | |
46 | 45 | rmo4 | |
47 | 38 46 | sylibr | |