Metamath Proof Explorer

Theorem lubval

Description: Value of the least upper 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. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

Ref Expression
Hypotheses lubval.b 
|- B = ( Base ` K )
lubval.l 
|- .<_ = ( le ` K )
lubval.u 
|- U = ( lub ` K )
lubval.p 
|- ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
lubval.k 
|- ( ph -> K e. V )
lubval.s 
|- ( ph -> S C_ B )
Assertion lubval 
|- ( ph -> ( U ` S ) = ( iota_ x e. B ps ) )

Proof

Step Hyp Ref Expression
1 lubval.b 
 |-  B = ( Base ` K )
2 lubval.l 
 |-  .<_ = ( le ` K )
3 lubval.u 
 |-  U = ( lub ` K )
4 lubval.p 
 |-  ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
5 lubval.k 
 |-  ( ph -> K e. V )
6 lubval.s 
 |-  ( ph -> S C_ B )
7 biid 
 |-  ( ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) <-> ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) )
8 5 adantr 
 |-  ( ( ph /\ S e. dom U ) -> K e. V )
9 1 2 3 7 8 lubfval 
 |-  ( ( ph /\ S e. dom U ) -> U = ( ( 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 ) ) } ) )
10 9 fveq1d 
 |-  ( ( ph /\ S e. dom U ) -> ( U ` S ) = ( ( ( 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 ) ) } ) ` S ) )
11 simpr 
 |-  ( ( ph /\ S e. dom U ) -> S e. dom U )
12 1 2 3 4 8 11 lubeu 
 |-  ( ( ph /\ S e. dom U ) -> E! x e. B ps )
13 raleq 
 |-  ( s = S -> ( A. y e. s y .<_ x <-> A. y e. S y .<_ x ) )
14 raleq 
 |-  ( s = S -> ( A. y e. s y .<_ z <-> A. y e. S y .<_ z ) )
15 14 imbi1d 
 |-  ( s = S -> ( ( A. y e. s y .<_ z -> x .<_ z ) <-> ( A. y e. S y .<_ z -> x .<_ z ) ) )
16 15 ralbidv 
 |-  ( s = S -> ( A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) <-> A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
17 13 16 anbi12d 
 |-  ( s = S -> ( ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) )
18 17 4 bitr4di 
 |-  ( s = S -> ( ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) <-> ps ) )
19 18 reubidv 
 |-  ( s = S -> ( E! x e. B ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) <-> E! x e. B ps ) )
20 11 12 19 elabd 
 |-  ( ( ph /\ S e. dom U ) -> S e. { s | E! x e. B ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) } )
21 20 fvresd 
 |-  ( ( ph /\ S e. dom U ) -> ( ( ( 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 ) ) } ) ` S ) = ( ( 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 ) )
22 6 adantr 
 |-  ( ( ph /\ S e. dom U ) -> 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 U ) -> S e. ~P B )
26 18 riotabidv 
 |-  ( s = S -> ( iota_ x e. B ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) ) = ( iota_ x e. B ps ) )
27 eqid 
 |-  ( 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. ~P B |-> ( iota_ x e. B ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) ) )
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 y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) ) ) ` S ) = ( iota_ x e. B ps ) )
30 25 29 syl 
 |-  ( ( ph /\ S e. dom U ) -> ( ( 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 ) = ( iota_ x e. B ps ) )
31 10 21 30 3eqtrd 
 |-  ( ( ph /\ S e. dom U ) -> ( U ` S ) = ( iota_ x e. B ps ) )
32 ndmfv 
 |-  ( -. S e. dom U -> ( U ` S ) = (/) )
33 32 adantl 
 |-  ( ( ph /\ -. S e. dom U ) -> ( U ` S ) = (/) )
34 1 2 3 4 5 lubeldm 
 |-  ( ph -> ( S e. dom U <-> ( S C_ B /\ E! x e. B ps ) ) )
35 34 biimprd 
 |-  ( ph -> ( ( S C_ B /\ E! x e. B ps ) -> S e. dom U ) )
36 6 35 mpand 
 |-  ( ph -> ( E! x e. B ps -> S e. dom U ) )
37 36 con3dimp 
 |-  ( ( ph /\ -. S e. dom U ) -> -. 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 U ) -> ( iota_ x e. B ps ) = (/) )
40 33 39 eqtr4d 
 |-  ( ( ph /\ -. S e. dom U ) -> ( U ` S ) = ( iota_ x e. B ps ) )
41 31 40 pm2.61dan 
 |-  ( ph -> ( U ` S ) = ( iota_ x e. B ps ) )