Metamath Proof Explorer


Theorem glbval

Description: Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying S e. dom U ) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

Ref Expression
Hypotheses glbval.b
|- B = ( Base ` K )
glbval.l
|- .<_ = ( le ` K )
glbval.g
|- G = ( glb ` K )
glbval.p
|- ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
glbva.k
|- ( ph -> K e. V )
glbval.ss
|- ( ph -> S C_ B )
Assertion glbval
|- ( ph -> ( G ` S ) = ( iota_ x e. B ps ) )

Proof

Step Hyp Ref Expression
1 glbval.b
 |-  B = ( Base ` K )
2 glbval.l
 |-  .<_ = ( le ` K )
3 glbval.g
 |-  G = ( glb ` K )
4 glbval.p
 |-  ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
5 glbva.k
 |-  ( ph -> K e. V )
6 glbval.ss
 |-  ( ph -> S C_ B )
7 biid
 |-  ( ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
8 5 adantr
 |-  ( ( ph /\ S e. dom G ) -> K e. V )
9 1 2 3 7 8 glbfval
 |-  ( ( ph /\ S e. dom G ) -> G = ( ( s e. ~P B |-> ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) ) |` { s | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } ) )
10 9 fveq1d
 |-  ( ( ph /\ S e. dom G ) -> ( G ` S ) = ( ( ( s e. ~P B |-> ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) ) |` { s | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } ) ` S ) )
11 simpr
 |-  ( ( ph /\ S e. dom G ) -> S e. dom G )
12 1 2 3 4 8 11 glbeu
 |-  ( ( ph /\ S e. dom G ) -> E! x e. B ps )
13 raleq
 |-  ( s = S -> ( A. y e. s x .<_ y <-> A. y e. S x .<_ y ) )
14 raleq
 |-  ( s = S -> ( A. y e. s z .<_ y <-> A. y e. S z .<_ y ) )
15 14 imbi1d
 |-  ( s = S -> ( ( A. y e. s z .<_ y -> z .<_ x ) <-> ( A. y e. S z .<_ y -> z .<_ x ) ) )
16 15 ralbidv
 |-  ( s = S -> ( A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) <-> A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
17 13 16 anbi12d
 |-  ( s = S -> ( ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) )
18 17 4 bitr4di
 |-  ( s = S -> ( ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> ps ) )
19 18 reubidv
 |-  ( s = S -> ( E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> E! x e. B ps ) )
20 11 12 19 elabd
 |-  ( ( ph /\ S e. dom G ) -> S e. { s | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } )
21 20 fvresd
 |-  ( ( ph /\ S e. dom G ) -> ( ( ( s e. ~P B |-> ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) ) |` { s | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } ) ` S ) = ( ( s e. ~P B |-> ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) ) ` S ) )
22 6 adantr
 |-  ( ( ph /\ S e. dom G ) -> S C_ B )
23 1 fvexi
 |-  B e. _V
24 23 elpw2
 |-  ( S e. ~P B <-> S C_ B )
25 22 24 sylibr
 |-  ( ( ph /\ S e. dom G ) -> S e. ~P B )
26 18 riotabidv
 |-  ( s = S -> ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) = ( iota_ x e. B ps ) )
27 eqid
 |-  ( s e. ~P B |-> ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) ) = ( s e. ~P B |-> ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) )
28 riotaex
 |-  ( iota_ x e. B ps ) e. _V
29 26 27 28 fvmpt
 |-  ( S e. ~P B -> ( ( s e. ~P B |-> ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) ) ` S ) = ( iota_ x e. B ps ) )
30 25 29 syl
 |-  ( ( ph /\ S e. dom G ) -> ( ( s e. ~P B |-> ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) ) ` S ) = ( iota_ x e. B ps ) )
31 10 21 30 3eqtrd
 |-  ( ( ph /\ S e. dom G ) -> ( G ` S ) = ( iota_ x e. B ps ) )
32 ndmfv
 |-  ( -. S e. dom G -> ( G ` S ) = (/) )
33 32 adantl
 |-  ( ( ph /\ -. S e. dom G ) -> ( G ` S ) = (/) )
34 1 2 3 4 5 glbeldm
 |-  ( ph -> ( S e. dom G <-> ( S C_ B /\ E! x e. B ps ) ) )
35 34 biimprd
 |-  ( ph -> ( ( S C_ B /\ E! x e. B ps ) -> S e. dom G ) )
36 6 35 mpand
 |-  ( ph -> ( E! x e. B ps -> S e. dom G ) )
37 36 con3dimp
 |-  ( ( ph /\ -. S e. dom G ) -> -. E! x e. B ps )
38 riotaund
 |-  ( -. E! x e. B ps -> ( iota_ x e. B ps ) = (/) )
39 37 38 syl
 |-  ( ( ph /\ -. S e. dom G ) -> ( iota_ x e. B ps ) = (/) )
40 33 39 eqtr4d
 |-  ( ( ph /\ -. S e. dom G ) -> ( G ` S ) = ( iota_ x e. B ps ) )
41 31 40 pm2.61dan
 |-  ( ph -> ( G ` S ) = ( iota_ x e. B ps ) )