This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )