Step |
Hyp |
Ref |
Expression |
1 |
|
supfirege.1 |
|- ( ph -> B C_ RR ) |
2 |
|
supfirege.2 |
|- ( ph -> B e. Fin ) |
3 |
|
supfirege.3 |
|- ( ph -> C e. B ) |
4 |
|
supfirege.4 |
|- ( ph -> S = sup ( B , RR , < ) ) |
5 |
|
ltso |
|- < Or RR |
6 |
5
|
a1i |
|- ( ph -> < Or RR ) |
7 |
6 1 2 3 4
|
supgtoreq |
|- ( ph -> ( C < S \/ C = S ) ) |
8 |
1 3
|
sseldd |
|- ( ph -> C e. RR ) |
9 |
3
|
ne0d |
|- ( ph -> B =/= (/) ) |
10 |
|
fisupcl |
|- ( ( < Or RR /\ ( B e. Fin /\ B =/= (/) /\ B C_ RR ) ) -> sup ( B , RR , < ) e. B ) |
11 |
6 2 9 1 10
|
syl13anc |
|- ( ph -> sup ( B , RR , < ) e. B ) |
12 |
4 11
|
eqeltrd |
|- ( ph -> S e. B ) |
13 |
1 12
|
sseldd |
|- ( ph -> S e. RR ) |
14 |
8 13
|
leloed |
|- ( ph -> ( C <_ S <-> ( C < S \/ C = S ) ) ) |
15 |
7 14
|
mpbird |
|- ( ph -> C <_ S ) |