Metamath Proof Explorer

Theorem poslubd

Description: Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses 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 poslubd 
|- ( ph -> ( U ` S ) = T )

Proof

Step Hyp Ref Expression
1 poslubd.l 
 |-  .<_ = ( le ` K )
2 poslubd.b 
 |-  B = ( Base ` K )
3 poslubd.u 
 |-  U = ( lub ` K )
4 poslubd.k 
 |-  ( ph -> K e. Poset )
5 poslubd.s 
 |-  ( ph -> S C_ B )
6 poslubd.t 
 |-  ( ph -> T e. B )
7 poslubd.ub 
 |-  ( ( ph /\ x e. S ) -> x .<_ T )
8 poslubd.le 
 |-  ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y )
9 biid 
 |-  ( ( 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 ) ) )
10 2 1 3 9 4 5 lubval 
 |-  ( 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 ) ) ) )
11 7 ralrimiva 
 |-  ( ph -> A. x e. S x .<_ T )
12 8 3expia 
 |-  ( ( ph /\ y e. B ) -> ( A. x e. S x .<_ y -> T .<_ y ) )
13 12 ralrimiva 
 |-  ( ph -> A. y e. B ( A. x e. S x .<_ y -> T .<_ y ) )
14 11 13 jca 
 |-  ( ph -> ( A. x e. S x .<_ T /\ A. y e. B ( A. x e. S x .<_ y -> T .<_ y ) ) )
15 breq2 
 |-  ( z = T -> ( x .<_ z <-> x .<_ T ) )
16 15 ralbidv 
 |-  ( z = T -> ( A. x e. S x .<_ z <-> A. x e. S x .<_ T ) )
17 breq1 
 |-  ( z = T -> ( z .<_ y <-> T .<_ y ) )
18 17 imbi2d 
 |-  ( z = T -> ( ( A. x e. S x .<_ y -> z .<_ y ) <-> ( A. x e. S x .<_ y -> T .<_ y ) ) )
19 18 ralbidv 
 |-  ( 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 ) ) )
20 16 19 anbi12d 
 |-  ( 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 ) ) ) )
21 20 rspcev 
 |-  ( ( 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 ) ) )
22 6 14 21 syl2anc 
 |-  ( ph -> E. z e. B ( A. x e. S x .<_ z /\ A. y e. B ( A. x e. S x .<_ y -> z .<_ y ) ) )
23 1 2 poslubmo 
 |-  ( ( 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 ) ) )
24 4 5 23 syl2anc 
 |-  ( 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 
 |-  ( 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 ) ) ) )
26 22 24 25 sylanbrc 
 |-  ( ph -> E! z e. B ( A. x e. S x .<_ z /\ A. y e. B ( A. x e. S x .<_ y -> z .<_ y ) ) )
27 20 riota2 
 |-  ( ( 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 ) )
28 6 26 27 syl2anc 
 |-  ( 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 ) )
29 14 28 mpbid 
 |-  ( ph -> ( iota_ z e. B ( A. x e. S x .<_ z /\ A. y e. B ( A. x e. S x .<_ y -> z .<_ y ) ) ) = T )
30 10 29 eqtrd 
 |-  ( ph -> ( U ` S ) = T )