This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )
17 10 adantr 
 |-  ( ( 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 )
24 23 adantlr 
 |-  ( ( ( 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. )