Metamath Proof Explorer

Theorem posglbmo

Description: Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018)

Ref Expression
Hypotheses poslubmo.l 
|- .<_ = ( le ` K )
poslubmo.b 
|- B = ( Base ` K )
Assertion posglbmo 
|- ( ( K e. Poset /\ S C_ B ) -> E* x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )

Proof

Step Hyp Ref Expression
1 poslubmo.l 
 |-  .<_ = ( le ` K )
2 poslubmo.b 
 |-  B = ( Base ` K )
3 simprrl 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> A. y e. S w .<_ y )
4 breq1 
 |-  ( z = w -> ( z .<_ y <-> w .<_ y ) )
5 4 ralbidv 
 |-  ( z = w -> ( A. y e. S z .<_ y <-> A. y e. S w .<_ y ) )
6 breq1 
 |-  ( z = w -> ( z .<_ x <-> w .<_ x ) )
7 5 6 imbi12d 
 |-  ( z = w -> ( ( A. y e. S z .<_ y -> z .<_ x ) <-> ( A. y e. S w .<_ y -> w .<_ x ) ) )
8 simprlr 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) )
9 simplrr 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> w e. B )
10 7 8 9 rspcdva 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> ( A. y e. S w .<_ y -> w .<_ x ) )
11 3 10 mpd 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> w .<_ x )
12 simprll 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> A. y e. S x .<_ y )
13 breq1 
 |-  ( z = x -> ( z .<_ y <-> x .<_ y ) )
14 13 ralbidv 
 |-  ( z = x -> ( A. y e. S z .<_ y <-> A. y e. S x .<_ y ) )
15 breq1 
 |-  ( z = x -> ( z .<_ w <-> x .<_ w ) )
16 14 15 imbi12d 
 |-  ( z = x -> ( ( A. y e. S z .<_ y -> z .<_ w ) <-> ( A. y e. S x .<_ y -> x .<_ w ) ) )
17 simprrr 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) )
18 simplrl 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> x e. B )
19 16 17 18 rspcdva 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> ( A. y e. S x .<_ y -> x .<_ w ) )
20 12 19 mpd 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> x .<_ w )
21 ancom 
 |-  ( ( w .<_ x /\ x .<_ w ) <-> ( x .<_ w /\ w .<_ x ) )
22 2 1 posasymb 
 |-  ( ( K e. Poset /\ x e. B /\ w e. B ) -> ( ( x .<_ w /\ w .<_ x ) <-> x = w ) )
23 21 22 bitrid 
 |-  ( ( K e. Poset /\ x e. B /\ w e. B ) -> ( ( w .<_ x /\ x .<_ w ) <-> x = w ) )
24 23 3expb 
 |-  ( ( K e. Poset /\ ( x e. B /\ w e. B ) ) -> ( ( w .<_ x /\ x .<_ w ) <-> x = w ) )
25 24 ad4ant13 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> ( ( w .<_ x /\ x .<_ w ) <-> x = w ) )
26 11 20 25 mpbi2and 
 |-  ( ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) /\ ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) ) -> x = w )
27 26 ex 
 |-  ( ( ( K e. Poset /\ S C_ B ) /\ ( x e. B /\ w e. B ) ) -> ( ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) -> x = w ) )
28 27 ralrimivva 
 |-  ( ( K e. Poset /\ S C_ B ) -> A. x e. B A. w e. B ( ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) -> x = w ) )
29 breq1 
 |-  ( x = w -> ( x .<_ y <-> w .<_ y ) )
30 29 ralbidv 
 |-  ( x = w -> ( A. y e. S x .<_ y <-> A. y e. S w .<_ y ) )
31 breq2 
 |-  ( x = w -> ( z .<_ x <-> z .<_ w ) )
32 31 imbi2d 
 |-  ( x = w -> ( ( A. y e. S z .<_ y -> z .<_ x ) <-> ( A. y e. S z .<_ y -> z .<_ w ) ) )
33 32 ralbidv 
 |-  ( x = w -> ( A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) <-> A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) )
34 30 33 anbi12d 
 |-  ( x = w -> ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) <-> ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) )
35 34 rmo4 
 |-  ( E* x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) <-> A. x e. B A. w e. B ( ( ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) /\ ( A. y e. S w .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ w ) ) ) -> x = w ) )
36 28 35 sylibr 
 |-  ( ( K e. Poset /\ S C_ B ) -> E* x e. B ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )