Metamath Proof Explorer

Theorem glb0N

Description: The greatest lower bound of the empty set is the unity element. (Contributed by NM, 5-Dec-2011) (New usage is discouraged.)

Ref Expression
Hypotheses glb0.g 
|- G = ( glb ` K )
glb0.u 
|- .1. = ( 1. ` K )
Assertion glb0N 
|- ( K e. OP -> ( G ` (/) ) = .1. )

Proof

Step Hyp Ref Expression
1 glb0.g 
 |-  G = ( glb ` K )
2 glb0.u 
 |-  .1. = ( 1. ` K )
3 eqid 
 |-  ( Base ` K ) = ( Base ` K )
4 eqid 
 |-  ( le ` K ) = ( le ` K )
5 biid 
 |-  ( ( A. y e. (/) x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) ) <-> ( A. y e. (/) x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) ) )
6 id 
 |-  ( K e. OP -> K e. OP )
7 0ss 
 |-  (/) C_ ( Base ` K )
8 7 a1i 
 |-  ( K e. OP -> (/) C_ ( Base ` K ) )
9 3 4 1 5 6 8 glbval 
 |-  ( K e. OP -> ( G ` (/) ) = ( iota_ x e. ( Base ` K ) ( A. y e. (/) x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) ) ) )
10 3 2 op1cl 
 |-  ( K e. OP -> .1. e. ( Base ` K ) )
11 ral0 
 |-  A. y e. (/) z ( le ` K ) y
12 11 a1bi 
 |-  ( z ( le ` K ) x <-> ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) )
13 12 ralbii 
 |-  ( A. z e. ( Base ` K ) z ( le ` K ) x <-> A. z e. ( Base ` K ) ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) )
14 ral0 
 |-  A. y e. (/) x ( le ` K ) y
15 14 biantrur 
 |-  ( A. z e. ( Base ` K ) ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) <-> ( A. y e. (/) x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) ) )
16 13 15 bitri 
 |-  ( A. z e. ( Base ` K ) z ( le ` K ) x <-> ( A. y e. (/) x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) ) )
17 10 adantr 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> .1. e. ( Base ` K ) )
18 breq1 
 |-  ( z = .1. -> ( z ( le ` K ) x <-> .1. ( le ` K ) x ) )
19 18 rspcv 
 |-  ( .1. e. ( Base ` K ) -> ( A. z e. ( Base ` K ) z ( le ` K ) x -> .1. ( le ` K ) x ) )
20 17 19 syl 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( A. z e. ( Base ` K ) z ( le ` K ) x -> .1. ( le ` K ) x ) )
21 3 4 2 op1le 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( .1. ( le ` K ) x <-> x = .1. ) )
22 20 21 sylibd 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( A. z e. ( Base ` K ) z ( le ` K ) x -> x = .1. ) )
23 3 4 2 ople1 
 |-  ( ( K e. OP /\ z e. ( Base ` K ) ) -> z ( le ` K ) .1. )
24 23 adantlr 
 |-  ( ( ( K e. OP /\ x e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> z ( le ` K ) .1. )
25 24 ex 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( z e. ( Base ` K ) -> z ( le ` K ) .1. ) )
26 breq2 
 |-  ( x = .1. -> ( z ( le ` K ) x <-> z ( le ` K ) .1. ) )
27 26 biimprcd 
 |-  ( z ( le ` K ) .1. -> ( x = .1. -> z ( le ` K ) x ) )
28 25 27 syl6 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( z e. ( Base ` K ) -> ( x = .1. -> z ( le ` K ) x ) ) )
29 28 com23 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( x = .1. -> ( z e. ( Base ` K ) -> z ( le ` K ) x ) ) )
30 29 ralrimdv 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( x = .1. -> A. z e. ( Base ` K ) z ( le ` K ) x ) )
31 22 30 impbid 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( A. z e. ( Base ` K ) z ( le ` K ) x <-> x = .1. ) )
32 16 31 bitr3id 
 |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( ( A. y e. (/) x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) ) <-> x = .1. ) )
33 10 32 riota5 
 |-  ( K e. OP -> ( iota_ x e. ( Base ` K ) ( A. y e. (/) x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. (/) z ( le ` K ) y -> z ( le ` K ) x ) ) ) = .1. )
34 9 33 eqtrd 
 |-  ( K e. OP -> ( G ` (/) ) = .1. )