Metamath Proof Explorer

Theorem supinf

Description: The supremum is the infimum of the upper bounds. (Contributed by SN, 29-Jun-2025)

Ref Expression
Hypotheses supinf.1 
|- ( ph -> .< Or A )
supinf.2 
|- ( ph -> E. x e. A ( A. y e. B -. x .< y /\ A. y e. A ( y .< x -> E. z e. B y .< z ) ) )
Assertion supinf 
|- ( ph -> sup ( B , A , .< ) = inf ( { x e. A | A. w e. B -. x .< w } , A , .< ) )

Proof

Step Hyp Ref Expression
1 supinf.1 
 |-  ( ph -> .< Or A )
2 supinf.2 
 |-  ( ph -> E. x e. A ( A. y e. B -. x .< y /\ A. y e. A ( y .< x -> E. z e. B y .< z ) ) )
3 1 2 supcl 
 |-  ( ph -> sup ( B , A , .< ) e. A )
4 breq1 
 |-  ( x = sup ( B , A , .< ) -> ( x .< w <-> sup ( B , A , .< ) .< w ) )
5 4 notbid 
 |-  ( x = sup ( B , A , .< ) -> ( -. x .< w <-> -. sup ( B , A , .< ) .< w ) )
6 5 ralbidv 
 |-  ( x = sup ( B , A , .< ) -> ( A. w e. B -. x .< w <-> A. w e. B -. sup ( B , A , .< ) .< w ) )
7 1 2 supub 
 |-  ( ph -> ( v e. B -> -. sup ( B , A , .< ) .< v ) )
8 7 ralrimiv 
 |-  ( ph -> A. v e. B -. sup ( B , A , .< ) .< v )
9 breq2 
 |-  ( v = w -> ( sup ( B , A , .< ) .< v <-> sup ( B , A , .< ) .< w ) )
10 9 notbid 
 |-  ( v = w -> ( -. sup ( B , A , .< ) .< v <-> -. sup ( B , A , .< ) .< w ) )
11 10 cbvralvw 
 |-  ( A. v e. B -. sup ( B , A , .< ) .< v <-> A. w e. B -. sup ( B , A , .< ) .< w )
12 8 11 sylib 
 |-  ( ph -> A. w e. B -. sup ( B , A , .< ) .< w )
13 6 3 12 elrabd 
 |-  ( ph -> sup ( B , A , .< ) e. { x e. A | A. w e. B -. x .< w } )
14 breq1 
 |-  ( x = v -> ( x .< w <-> v .< w ) )
15 14 notbid 
 |-  ( x = v -> ( -. x .< w <-> -. v .< w ) )
16 15 ralbidv 
 |-  ( x = v -> ( A. w e. B -. x .< w <-> A. w e. B -. v .< w ) )
17 16 elrab 
 |-  ( v e. { x e. A | A. w e. B -. x .< w } <-> ( v e. A /\ A. w e. B -. v .< w ) )
18 breq2 
 |-  ( z = w -> ( y .< z <-> y .< w ) )
19 18 cbvrexvw 
 |-  ( E. z e. B y .< z <-> E. w e. B y .< w )
20 19 imbi2i 
 |-  ( ( y .< x -> E. z e. B y .< z ) <-> ( y .< x -> E. w e. B y .< w ) )
21 20 ralbii 
 |-  ( A. y e. A ( y .< x -> E. z e. B y .< z ) <-> A. y e. A ( y .< x -> E. w e. B y .< w ) )
22 21 anbi2i 
 |-  ( ( A. y e. B -. x .< y /\ A. y e. A ( y .< x -> E. z e. B y .< z ) ) <-> ( A. y e. B -. x .< y /\ A. y e. A ( y .< x -> E. w e. B y .< w ) ) )
23 22 rexbii 
 |-  ( E. x e. A ( A. y e. B -. x .< y /\ A. y e. A ( y .< x -> E. z e. B y .< z ) ) <-> E. x e. A ( A. y e. B -. x .< y /\ A. y e. A ( y .< x -> E. w e. B y .< w ) ) )
24 2 23 sylib 
 |-  ( ph -> E. x e. A ( A. y e. B -. x .< y /\ A. y e. A ( y .< x -> E. w e. B y .< w ) ) )
25 1 24 supnub 
 |-  ( ph -> ( ( v e. A /\ A. w e. B -. v .< w ) -> -. v .< sup ( B , A , .< ) ) )
26 17 25 biimtrid 
 |-  ( ph -> ( v e. { x e. A | A. w e. B -. x .< w } -> -. v .< sup ( B , A , .< ) ) )
27 26 imp 
 |-  ( ( ph /\ v e. { x e. A | A. w e. B -. x .< w } ) -> -. v .< sup ( B , A , .< ) )
28 1 3 13 27 infmin 
 |-  ( ph -> inf ( { x e. A | A. w e. B -. x .< w } , A , .< ) = sup ( B , A , .< ) )
29 28 eqcomd 
 |-  ( ph -> sup ( B , A , .< ) = inf ( { x e. A | A. w e. B -. x .< w } , A , .< ) )