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 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 K = K
5 biid y y K x z Base K y y K z x K z y y K x z Base K y y K z x K z
6 id K OP K OP
7 0ss Base K
8 7 a1i K OP Base K
9 3 4 1 5 6 8 lubval K OP 1 ˙ = ι x Base K | y y K x z Base K y y K z x K z
10 3 2 op0cl K OP 0 ˙ Base K
11 ral0 y y K z
12 11 a1bi x K z y y K z x K z
13 12 ralbii z Base K x K z z Base K y y K z x K z
14 ral0 y y K x
15 14 biantrur z Base K y y K z x K z y y K x z Base K y y K z x K z
16 13 15 bitri z Base K x K z y y K x z Base K y y K z x K z
17 10 adantr K OP x Base K 0 ˙ Base K
18 breq2 z = 0 ˙ x K z x K 0 ˙
19 18 rspcv 0 ˙ Base K z Base K x K z x K 0 ˙
20 17 19 syl K OP x Base K z Base K x K z x K 0 ˙
21 3 4 2 ople0 K OP x Base K x K 0 ˙ x = 0 ˙
22 20 21 sylibd K OP x Base K z Base K x K z x = 0 ˙
23 3 4 2 op0le K OP z Base K 0 ˙ K z
24 23 adantlr K OP x Base K z Base K 0 ˙ K z
25 24 ex K OP x Base K z Base K 0 ˙ K z
26 breq1 x = 0 ˙ x K z 0 ˙ K z
27 26 biimprcd 0 ˙ K z x = 0 ˙ x K z
28 25 27 syl6 K OP x Base K z Base K x = 0 ˙ x K z
29 28 com23 K OP x Base K x = 0 ˙ z Base K x K z
30 29 ralrimdv K OP x Base K x = 0 ˙ z Base K x K z
31 22 30 impbid K OP x Base K z Base K x K z x = 0 ˙
32 16 31 bitr3id K OP x Base K y y K x z Base K y y K z x K z x = 0 ˙
33 10 32 riota5 K OP ι x Base K | y y K x z Base K y y K z x K z = 0 ˙
34 9 33 eqtrd K OP 1 ˙ = 0 ˙