Metamath Proof Explorer


Theorem supgtoreq

Description: The supremum of a finite set is greater than or equal to all the elements of the set. (Contributed by AV, 1-Oct-2019)

Ref Expression
Hypotheses supgtoreq.1
|- ( ph -> R Or A )
supgtoreq.2
|- ( ph -> B C_ A )
supgtoreq.3
|- ( ph -> B e. Fin )
supgtoreq.4
|- ( ph -> C e. B )
supgtoreq.5
|- ( ph -> S = sup ( B , A , R ) )
Assertion supgtoreq
|- ( ph -> ( C R S \/ C = S ) )

Proof

Step Hyp Ref Expression
1 supgtoreq.1
 |-  ( ph -> R Or A )
2 supgtoreq.2
 |-  ( ph -> B C_ A )
3 supgtoreq.3
 |-  ( ph -> B e. Fin )
4 supgtoreq.4
 |-  ( ph -> C e. B )
5 supgtoreq.5
 |-  ( ph -> S = sup ( B , A , R ) )
6 4 ne0d
 |-  ( ph -> B =/= (/) )
7 fisup2g
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E. x e. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
8 1 3 6 2 7 syl13anc
 |-  ( ph -> E. x e. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
9 ssrexv
 |-  ( B C_ A -> ( E. x e. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
10 2 8 9 sylc
 |-  ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
11 1 10 supub
 |-  ( ph -> ( C e. B -> -. sup ( B , A , R ) R C ) )
12 4 11 mpd
 |-  ( ph -> -. sup ( B , A , R ) R C )
13 5 12 eqnbrtrd
 |-  ( ph -> -. S R C )
14 fisupcl
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , R ) e. B )
15 1 3 6 2 14 syl13anc
 |-  ( ph -> sup ( B , A , R ) e. B )
16 2 15 sseldd
 |-  ( ph -> sup ( B , A , R ) e. A )
17 5 16 eqeltrd
 |-  ( ph -> S e. A )
18 2 4 sseldd
 |-  ( ph -> C e. A )
19 sotric
 |-  ( ( R Or A /\ ( S e. A /\ C e. A ) ) -> ( S R C <-> -. ( S = C \/ C R S ) ) )
20 1 17 18 19 syl12anc
 |-  ( ph -> ( S R C <-> -. ( S = C \/ C R S ) ) )
21 orcom
 |-  ( ( S = C \/ C R S ) <-> ( C R S \/ S = C ) )
22 eqcom
 |-  ( S = C <-> C = S )
23 22 orbi2i
 |-  ( ( C R S \/ S = C ) <-> ( C R S \/ C = S ) )
24 21 23 bitri
 |-  ( ( S = C \/ C R S ) <-> ( C R S \/ C = S ) )
25 24 notbii
 |-  ( -. ( S = C \/ C R S ) <-> -. ( C R S \/ C = S ) )
26 20 25 bitr2di
 |-  ( ph -> ( -. ( C R S \/ C = S ) <-> S R C ) )
27 13 26 mtbird
 |-  ( ph -> -. -. ( C R S \/ C = S ) )
28 27 notnotrd
 |-  ( ph -> ( C R S \/ C = S ) )