MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  poslubd Structured version   Visualization version   Unicode version

Theorem poslubd 16406
Description: Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
Hypotheses
Ref Expression
poslubd.l  |-  .<_  =  ( le `  K )
poslubd.b  |-  B  =  ( Base `  K
)
poslubd.u  |-  U  =  ( lub `  K
)
poslubd.k  |-  ( ph  ->  K  e.  Poset )
poslubd.s  |-  ( ph  ->  S  C_  B )
poslubd.t  |-  ( ph  ->  T  e.  B )
poslubd.ub  |-  ( (
ph  /\  x  e.  S )  ->  x  .<_  T )
poslubd.le  |-  ( (
ph  /\  y  e.  B  /\  A. x  e.  S  x  .<_  y )  ->  T  .<_  y )
Assertion
Ref Expression
poslubd  |-  ( ph  ->  ( U `  S
)  =  T )
Distinct variable groups:    x,  .<_ , y   
x, B, y    x, K, y    x, S, y   
x, U, y    x, T, y    ph, x, y

Proof of Theorem poslubd
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 poslubd.b . . 3  |-  B  =  ( Base `  K
)
2 poslubd.l . . 3  |-  .<_  =  ( le `  K )
3 poslubd.u . . 3  |-  U  =  ( lub `  K
)
4 biid 240 . . 3  |-  ( ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) )  <->  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )
5 poslubd.k . . 3  |-  ( ph  ->  K  e.  Poset )
6 poslubd.s . . 3  |-  ( ph  ->  S  C_  B )
71, 2, 3, 4, 5, 6lubval 16242 . 2  |-  ( ph  ->  ( U `  S
)  =  ( iota_ z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) ) )
8 poslubd.ub . . . . 5  |-  ( (
ph  /\  x  e.  S )  ->  x  .<_  T )
98ralrimiva 2804 . . . 4  |-  ( ph  ->  A. x  e.  S  x  .<_  T )
10 poslubd.le . . . . . 6  |-  ( (
ph  /\  y  e.  B  /\  A. x  e.  S  x  .<_  y )  ->  T  .<_  y )
11103expia 1211 . . . . 5  |-  ( (
ph  /\  y  e.  B )  ->  ( A. x  e.  S  x  .<_  y  ->  T  .<_  y ) )
1211ralrimiva 2804 . . . 4  |-  ( ph  ->  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  T  .<_  y ) )
139, 12jca 535 . . 3  |-  ( ph  ->  ( A. x  e.  S  x  .<_  T  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  T  .<_  y ) ) )
14 poslubd.t . . . 4  |-  ( ph  ->  T  e.  B )
15 breq2 4409 . . . . . . . . 9  |-  ( z  =  T  ->  (
x  .<_  z  <->  x  .<_  T ) )
1615ralbidv 2829 . . . . . . . 8  |-  ( z  =  T  ->  ( A. x  e.  S  x  .<_  z  <->  A. x  e.  S  x  .<_  T ) )
17 breq1 4408 . . . . . . . . . 10  |-  ( z  =  T  ->  (
z  .<_  y  <->  T  .<_  y ) )
1817imbi2d 318 . . . . . . . . 9  |-  ( z  =  T  ->  (
( A. x  e.  S  x  .<_  y  -> 
z  .<_  y )  <->  ( A. x  e.  S  x  .<_  y  ->  T  .<_  y ) ) )
1918ralbidv 2829 . . . . . . . 8  |-  ( z  =  T  ->  ( A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y )  <->  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  T  .<_  y ) ) )
2016, 19anbi12d 718 . . . . . . 7  |-  ( z  =  T  ->  (
( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) )  <->  ( A. x  e.  S  x  .<_  T  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  T  .<_  y ) ) ) )
2120rspcev 3152 . . . . . 6  |-  ( ( T  e.  B  /\  ( A. x  e.  S  x  .<_  T  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  T  .<_  y ) ) )  ->  E. z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )
2214, 13, 21syl2anc 667 . . . . 5  |-  ( ph  ->  E. z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )
232, 1poslubmo 16404 . . . . . 6  |-  ( ( K  e.  Poset  /\  S  C_  B )  ->  E* z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )
245, 6, 23syl2anc 667 . . . . 5  |-  ( ph  ->  E* z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )
25 reu5 3010 . . . . 5  |-  ( E! z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) )  <->  ( E. z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) )  /\  E* z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) ) )
2622, 24, 25sylanbrc 671 . . . 4  |-  ( ph  ->  E! z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )
2720riota2 6279 . . . 4  |-  ( ( T  e.  B  /\  E! z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )  ->  ( ( A. x  e.  S  x  .<_  T  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  T  .<_  y ) )  <->  ( iota_ z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )  =  T ) )
2814, 26, 27syl2anc 667 . . 3  |-  ( ph  ->  ( ( A. x  e.  S  x  .<_  T  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  T  .<_  y ) )  <->  ( iota_ z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )  =  T ) )
2913, 28mpbid 214 . 2  |-  ( ph  ->  ( iota_ z  e.  B  ( A. x  e.  S  x  .<_  z  /\  A. y  e.  B  ( A. x  e.  S  x  .<_  y  ->  z  .<_  y ) ) )  =  T )
307, 29eqtrd 2487 1  |-  ( ph  ->  ( U `  S
)  =  T )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 986    = wceq 1446    e. wcel 1889   A.wral 2739   E.wrex 2740   E!wreu 2741   E*wrmo 2742    C_ wss 3406   class class class wbr 4405   ` cfv 5585   iota_crio 6256   Basecbs 15133   lecple 15209   Posetcpo 16197   lubclub 16199
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-riota 6257  df-preset 16185  df-poset 16203  df-lub 16232
This theorem is referenced by:  poslubdg  16407
  Copyright terms: Public domain W3C validator