Metamath Proof Explorer

Theorem tosglb

Description: Same theorem as toslub , for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018) (Revised by AV, 28-Sep-2020)

Ref Expression
Hypotheses tosglb.b 
|- B = ( Base ` K )
tosglb.l 
|- .< = ( lt ` K )
tosglb.1 
|- ( ph -> K e. Toset )
tosglb.2 
|- ( ph -> A C_ B )
Assertion tosglb 
|- ( ph -> ( ( glb ` K ) ` A ) = inf ( A , B , .< ) )

Proof

Step Hyp Ref Expression
1 tosglb.b 
 |-  B = ( Base ` K )
2 tosglb.l 
 |-  .< = ( lt ` K )
3 tosglb.1 
 |-  ( ph -> K e. Toset )
4 tosglb.2 
 |-  ( ph -> A C_ B )
5 eqid 
 |-  ( le ` K ) = ( le ` K )
6 1 2 3 4 5 tosglblem 
 |-  ( ( ph /\ a e. B ) -> ( ( A. b e. A a ( le ` K ) b /\ A. c e. B ( A. b e. A c ( le ` K ) b -> c ( le ` K ) a ) ) <-> ( A. b e. A -. a `' .< b /\ A. b e. B ( b `' .< a -> E. d e. A b `' .< d ) ) ) )
7 6 riotabidva 
 |-  ( ph -> ( iota_ a e. B ( A. b e. A a ( le ` K ) b /\ A. c e. B ( A. b e. A c ( le ` K ) b -> c ( le ` K ) a ) ) ) = ( iota_ a e. B ( A. b e. A -. a `' .< b /\ A. b e. B ( b `' .< a -> E. d e. A b `' .< d ) ) ) )
8 eqid 
 |-  ( glb ` K ) = ( glb ` K )
9 biid 
 |-  ( ( A. b e. A a ( le ` K ) b /\ A. c e. B ( A. b e. A c ( le ` K ) b -> c ( le ` K ) a ) ) <-> ( A. b e. A a ( le ` K ) b /\ A. c e. B ( A. b e. A c ( le ` K ) b -> c ( le ` K ) a ) ) )
10 1 5 8 9 3 4 glbval 
 |-  ( ph -> ( ( glb ` K ) ` A ) = ( iota_ a e. B ( A. b e. A a ( le ` K ) b /\ A. c e. B ( A. b e. A c ( le ` K ) b -> c ( le ` K ) a ) ) ) )
11 1 5 2 tosso 
 |-  ( K e. Toset -> ( K e. Toset <-> ( .< Or B /\ ( _I |` B ) C_ ( le ` K ) ) ) )
12 11 ibi 
 |-  ( K e. Toset -> ( .< Or B /\ ( _I |` B ) C_ ( le ` K ) ) )
13 12 simpld 
 |-  ( K e. Toset -> .< Or B )
14 cnvso 
 |-  ( .< Or B <-> `' .< Or B )
15 13 14 sylib 
 |-  ( K e. Toset -> `' .< Or B )
16 id 
 |-  ( `' .< Or B -> `' .< Or B )
17 16 supval2 
 |-  ( `' .< Or B -> sup ( A , B , `' .< ) = ( iota_ a e. B ( A. b e. A -. a `' .< b /\ A. b e. B ( b `' .< a -> E. d e. A b `' .< d ) ) ) )
18 3 15 17 3syl 
 |-  ( ph -> sup ( A , B , `' .< ) = ( iota_ a e. B ( A. b e. A -. a `' .< b /\ A. b e. B ( b `' .< a -> E. d e. A b `' .< d ) ) ) )
19 7 10 18 3eqtr4d 
 |-  ( ph -> ( ( glb ` K ) ` A ) = sup ( A , B , `' .< ) )
20 df-inf 
 |-  inf ( A , B , .< ) = sup ( A , B , `' .< )
21 20 eqcomi 
 |-  sup ( A , B , `' .< ) = inf ( A , B , .< )
22 21 a1i 
 |-  ( ph -> sup ( A , B , `' .< ) = inf ( A , B , .< ) )
23 19 22 eqtrd 
 |-  ( ph -> ( ( glb ` K ) ` A ) = inf ( A , B , .< ) )