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

Metamath Proof Explorer

Theorem infltoreq

Description: The infimum of a finite set is less than or equal to all the elements of the set. (Contributed by AV, 4-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 infltoreq.1 
 |-  ( ph -> R Or A )
2 infltoreq.2 
 |-  ( ph -> B C_ A )
3 infltoreq.3 
 |-  ( ph -> B e. Fin )
4 infltoreq.4 
 |-  ( ph -> C e. B )
5 infltoreq.5 
 |-  ( ph -> S = inf ( B , A , R ) )
6 cnvso 
 |-  ( R Or A <-> `' R Or A )
7 1 6 sylib 
 |-  ( ph -> `' R Or A )
8 df-inf 
 |-  inf ( B , A , R ) = sup ( B , A , `' R )
9 5 8 eqtrdi 
 |-  ( ph -> S = sup ( B , A , `' R ) )
10 7 2 3 4 9 supgtoreq 
 |-  ( ph -> ( C `' R S \/ C = S ) )
11 4 ne0d 
 |-  ( ph -> B =/= (/) )
12 fiinfcl 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> inf ( B , A , R ) e. B )
13 1 3 11 2 12 syl13anc 
 |-  ( ph -> inf ( B , A , R ) e. B )
14 5 13 eqeltrd 
 |-  ( ph -> S e. B )
15 brcnvg 
 |-  ( ( C e. B /\ S e. B ) -> ( C `' R S <-> S R C ) )
16 15 bicomd 
 |-  ( ( C e. B /\ S e. B ) -> ( S R C <-> C `' R S ) )
17 4 14 16 syl2anc 
 |-  ( ph -> ( S R C <-> C `' R S ) )
18 17 orbi1d 
 |-  ( ph -> ( ( S R C \/ C = S ) <-> ( C `' R S \/ C = S ) ) )
19 10 18 mpbird 
 |-  ( ph -> ( S R C \/ C = S ) )