Metamath Proof Explorer

Theorem suplub

Description: A supremum is the least upper bound. See also supcl and supub . (Contributed by NM, 13-Oct-2004) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supmo.1 
|- ( ph -> R Or A )
supcl.2 
|- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
Assertion suplub 
|- ( ph -> ( ( C e. A /\ C R sup ( B , A , R ) ) -> E. z e. B C R z ) )

Proof

Step Hyp Ref Expression
1 supmo.1 
 |-  ( ph -> R Or A )
2 supcl.2 
 |-  ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
3 simpr 
 |-  ( ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> A. y e. A ( y R x -> E. z e. B y R z ) )
4 breq1 
 |-  ( y = w -> ( y R x <-> w R x ) )
5 breq1 
 |-  ( y = w -> ( y R z <-> w R z ) )
6 5 rexbidv 
 |-  ( y = w -> ( E. z e. B y R z <-> E. z e. B w R z ) )
7 4 6 imbi12d 
 |-  ( y = w -> ( ( y R x -> E. z e. B y R z ) <-> ( w R x -> E. z e. B w R z ) ) )
8 7 cbvralvw 
 |-  ( A. y e. A ( y R x -> E. z e. B y R z ) <-> A. w e. A ( w R x -> E. z e. B w R z ) )
9 3 8 sylib 
 |-  ( ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> A. w e. A ( w R x -> E. z e. B w R z ) )
10 9 a1i 
 |-  ( x e. A -> ( ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> A. w e. A ( w R x -> E. z e. B w R z ) ) )
11 10 ss2rabi 
 |-  { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } C_ { x e. A | A. w e. A ( w R x -> E. z e. B w R z ) }
12 1 supval2 
 |-  ( ph -> sup ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
13 1 2 supeu 
 |-  ( ph -> E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
14 riotacl2 
 |-  ( E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) e. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } )
15 13 14 syl 
 |-  ( ph -> ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) e. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } )
16 12 15 eqeltrd 
 |-  ( ph -> sup ( B , A , R ) e. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } )
17 11 16 sseldi 
 |-  ( ph -> sup ( B , A , R ) e. { x e. A | A. w e. A ( w R x -> E. z e. B w R z ) } )
18 breq2 
 |-  ( x = sup ( B , A , R ) -> ( w R x <-> w R sup ( B , A , R ) ) )
19 18 imbi1d 
 |-  ( x = sup ( B , A , R ) -> ( ( w R x -> E. z e. B w R z ) <-> ( w R sup ( B , A , R ) -> E. z e. B w R z ) ) )
20 19 ralbidv 
 |-  ( x = sup ( B , A , R ) -> ( A. w e. A ( w R x -> E. z e. B w R z ) <-> A. w e. A ( w R sup ( B , A , R ) -> E. z e. B w R z ) ) )
21 20 elrab 
 |-  ( sup ( B , A , R ) e. { x e. A | A. w e. A ( w R x -> E. z e. B w R z ) } <-> ( sup ( B , A , R ) e. A /\ A. w e. A ( w R sup ( B , A , R ) -> E. z e. B w R z ) ) )
22 21 simprbi 
 |-  ( sup ( B , A , R ) e. { x e. A | A. w e. A ( w R x -> E. z e. B w R z ) } -> A. w e. A ( w R sup ( B , A , R ) -> E. z e. B w R z ) )
23 17 22 syl 
 |-  ( ph -> A. w e. A ( w R sup ( B , A , R ) -> E. z e. B w R z ) )
24 breq1 
 |-  ( w = C -> ( w R sup ( B , A , R ) <-> C R sup ( B , A , R ) ) )
25 breq1 
 |-  ( w = C -> ( w R z <-> C R z ) )
26 25 rexbidv 
 |-  ( w = C -> ( E. z e. B w R z <-> E. z e. B C R z ) )
27 24 26 imbi12d 
 |-  ( w = C -> ( ( w R sup ( B , A , R ) -> E. z e. B w R z ) <-> ( C R sup ( B , A , R ) -> E. z e. B C R z ) ) )
28 27 rspccv 
 |-  ( A. w e. A ( w R sup ( B , A , R ) -> E. z e. B w R z ) -> ( C e. A -> ( C R sup ( B , A , R ) -> E. z e. B C R z ) ) )
29 28 impd 
 |-  ( A. w e. A ( w R sup ( B , A , R ) -> E. z e. B w R z ) -> ( ( C e. A /\ C R sup ( B , A , R ) ) -> E. z e. B C R z ) )
30 23 29 syl 
 |-  ( ph -> ( ( C e. A /\ C R sup ( B , A , R ) ) -> E. z e. B C R z ) )