Metamath Proof Explorer

Theorem lubfval

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

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

Proof

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