Metamath Proof Explorer

Theorem glbfval

Description: Value of the greatest lower function of a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 6-Sep-2018)

Ref Expression
Hypotheses glbfval.b 
|- B = ( Base ` K )
glbfval.l 
|- .<_ = ( le ` K )
glbfval.g 
|- G = ( glb ` K )
glbfval.p 
|- ( ps <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
glbfval.k 
|- ( ph -> K e. V )
Assertion glbfval 
|- ( ph -> G = ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )

Proof

Step Hyp Ref Expression
1 glbfval.b 
 |-  B = ( Base ` K )
2 glbfval.l 
 |-  .<_ = ( le ` K )
3 glbfval.g 
 |-  G = ( glb ` K )
4 glbfval.p 
 |-  ( ps <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
5 glbfval.k 
 |-  ( ph -> K e. V )
6 elex 
 |-  ( K e. V -> K e. _V )
7 fveq2 
 |-  ( p = K -> ( Base ` p ) = ( Base ` K ) )
8 7 1 eqtr4di 
 |-  ( p = K -> ( Base ` p ) = B )
9 8 pweqd 
 |-  ( p = K -> ~P ( Base ` p ) = ~P B )
10 fveq2 
 |-  ( p = K -> ( le ` p ) = ( le ` K ) )
11 10 2 eqtr4di 
 |-  ( p = K -> ( le ` p ) = .<_ )
12 11 breqd 
 |-  ( p = K -> ( x ( le ` p ) y <-> x .<_ y ) )
13 12 ralbidv 
 |-  ( p = K -> ( A. y e. s x ( le ` p ) y <-> A. y e. s x .<_ y ) )
14 11 breqd 
 |-  ( p = K -> ( z ( le ` p ) y <-> z .<_ y ) )
15 14 ralbidv 
 |-  ( p = K -> ( A. y e. s z ( le ` p ) y <-> A. y e. s z .<_ y ) )
16 11 breqd 
 |-  ( p = K -> ( z ( le ` p ) x <-> z .<_ x ) )
17 15 16 imbi12d 
 |-  ( p = K -> ( ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) <-> ( A. y e. s z .<_ y -> z .<_ x ) ) )
18 8 17 raleqbidv 
 |-  ( p = K -> ( A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) <-> A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
19 13 18 anbi12d 
 |-  ( p = K -> ( ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) )
20 8 19 riotaeqbidv 
 |-  ( p = K -> ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) ) = ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) )
21 9 20 mpteq12dv 
 |-  ( p = K -> ( s e. ~P ( Base ` p ) |-> ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) 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 ) ) ) ) )
22 19 reubidv 
 |-  ( p = K -> ( E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) <-> E! x e. ( Base ` p ) ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) )
23 reueq1 
 |-  ( ( Base ` p ) = B -> ( E! x e. ( Base ` p ) ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) )
24 8 23 syl 
 |-  ( p = K -> ( E! x e. ( Base ` p ) ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) <-> E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) )
25 22 24 bitrd 
 |-  ( p = K -> ( E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) <-> E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) )
26 25 abbidv 
 |-  ( p = K -> { s | E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) } = { s | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } )
27 21 26 reseq12d 
 |-  ( p = K -> ( ( s e. ~P ( Base ` p ) |-> ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) ) ) |` { s | E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) 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 ) ) ) ) |` { s | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) } ) )
28 df-glb 
 |-  glb = ( p e. _V |-> ( ( s e. ~P ( Base ` p ) |-> ( iota_ x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) ) ) |` { s | E! x e. ( Base ` p ) ( A. y e. s x ( le ` p ) y /\ A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x ) ) } ) )
29 1 fvexi 
 |-  B e. _V
30 29 pwex 
 |-  ~P B e. _V
31 30 mptex 
 |-  ( 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 ) ) ) ) e. _V
32 31 resex 
 |-  ( ( 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 ) ) } ) e. _V
33 27 28 32 fvmpt 
 |-  ( K e. _V -> ( glb ` K ) = ( ( 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 ) ) } ) )
34 4 a1i 
 |-  ( x e. B -> ( ps <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) ) )
35 34 riotabiia 
 |-  ( iota_ x e. B ps ) = ( iota_ x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
36 35 mpteq2i 
 |-  ( s e. ~P B |-> ( iota_ x e. B ps ) ) = ( 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 ) ) ) )
37 4 reubii 
 |-  ( E! x e. B ps <-> E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
38 37 abbii 
 |-  { s | E! x e. B ps } = { s | E! x e. B ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) }
39 36 38 reseq12i 
 |-  ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) = ( ( 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 ) ) } )
40 33 3 39 3eqtr4g 
 |-  ( K e. _V -> G = ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )
41 5 6 40 3syl 
 |-  ( ph -> G = ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )