# Metamath Proof Explorer

## Theorem lub0N

Description: The least upper bound of the empty set is the zero element. (Contributed by NM, 15-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lub0.u
`|- .1. = ( lub ` K )`
lub0.z
`|- .0. = ( 0. ` K )`
Assertion lub0N
`|- ( K e. OP -> ( .1. ` (/) ) = .0. )`

### Proof

Step Hyp Ref Expression
1 lub0.u
` |-  .1. = ( lub ` K )`
2 lub0.z
` |-  .0. = ( 0. ` K )`
3 eqid
` |-  ( Base ` K ) = ( Base ` K )`
4 eqid
` |-  ( le ` K ) = ( le ` K )`
5 biid
` |-  ( ( A. y e. (/) y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) ) <-> ( A. y e. (/) y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) ) )`
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 lubval
` |-  ( K e. OP -> ( .1. ` (/) ) = ( iota_ x e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) ) ) )`
10 3 2 op0cl
` |-  ( K e. OP -> .0. e. ( Base ` K ) )`
11 ral0
` |-  A. y e. (/) y ( le ` K ) z`
12 11 a1bi
` |-  ( x ( le ` K ) z <-> ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) )`
13 12 ralbii
` |-  ( A. z e. ( Base ` K ) x ( le ` K ) z <-> A. z e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) )`
14 ral0
` |-  A. y e. (/) y ( le ` K ) x`
15 14 biantrur
` |-  ( A. z e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) <-> ( A. y e. (/) y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) ) )`
16 13 15 bitri
` |-  ( A. z e. ( Base ` K ) x ( le ` K ) z <-> ( A. y e. (/) y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) ) )`
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> .0. e. ( Base ` K ) )`
18 breq2
` |-  ( z = .0. -> ( x ( le ` K ) z <-> x ( le ` K ) .0. ) )`
19 18 rspcv
` |-  ( .0. e. ( Base ` K ) -> ( A. z e. ( Base ` K ) x ( le ` K ) z -> x ( le ` K ) .0. ) )`
20 17 19 syl
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( A. z e. ( Base ` K ) x ( le ` K ) z -> x ( le ` K ) .0. ) )`
21 3 4 2 ople0
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( x ( le ` K ) .0. <-> x = .0. ) )`
22 20 21 sylibd
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( A. z e. ( Base ` K ) x ( le ` K ) z -> x = .0. ) )`
23 3 4 2 op0le
` |-  ( ( K e. OP /\ z e. ( Base ` K ) ) -> .0. ( le ` K ) z )`
` |-  ( ( ( K e. OP /\ x e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> .0. ( le ` K ) z )`
25 24 ex
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( z e. ( Base ` K ) -> .0. ( le ` K ) z ) )`
26 breq1
` |-  ( x = .0. -> ( x ( le ` K ) z <-> .0. ( le ` K ) z ) )`
27 26 biimprcd
` |-  ( .0. ( le ` K ) z -> ( x = .0. -> x ( le ` K ) z ) )`
28 25 27 syl6
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( z e. ( Base ` K ) -> ( x = .0. -> x ( le ` K ) z ) ) )`
29 28 com23
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( x = .0. -> ( z e. ( Base ` K ) -> x ( le ` K ) z ) ) )`
30 29 ralrimdv
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( x = .0. -> A. z e. ( Base ` K ) x ( le ` K ) z ) )`
31 22 30 impbid
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( A. z e. ( Base ` K ) x ( le ` K ) z <-> x = .0. ) )`
32 16 31 bitr3id
` |-  ( ( K e. OP /\ x e. ( Base ` K ) ) -> ( ( A. y e. (/) y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) ) <-> x = .0. ) )`
33 10 32 riota5
` |-  ( K e. OP -> ( iota_ x e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. (/) y ( le ` K ) z -> x ( le ` K ) z ) ) ) = .0. )`
34 9 33 eqtrd
` |-  ( K e. OP -> ( .1. ` (/) ) = .0. )`