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 ˙