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