Metamath Proof Explorer

Theorem glb0N

Description: The greatest lower bound of the empty set is the unit 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 ∈ 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 ⊢ ≤ K = ≤ K
5 biid ⊢ ∀ y ∈ ∅ x ≤ K y ∧ ∀ z ∈ Base K ∀ y ∈ ∅ z ≤ K y → z ≤ K x ↔ ∀ y ∈ ∅ x ≤ K y ∧ ∀ z ∈ Base K ∀ y ∈ ∅ z ≤ K y → z ≤ K x
6 id ⊢ K ∈ OP → K ∈ OP
7 0ss ⊢ ∅ ⊆ Base K
8 7 a1i ⊢ K ∈ OP → ∅ ⊆ Base K
9 3 4 1 5 6 8 glbval ⊢ K ∈ OP → G ⁡ ∅ = ι x ∈ Base K | ∀ y ∈ ∅ x ≤ K y ∧ ∀ z ∈ Base K ∀ y ∈ ∅ z ≤ K y → z ≤ K x
10 3 2 op1cl ⊢ K ∈ OP → 1 ˙ ∈ Base K
11 ral0 ⊢ ∀ y ∈ ∅ z ≤ K y
12 11 a1bi ⊢ z ≤ K x ↔ ∀ y ∈ ∅ z ≤ K y → z ≤ K x
13 12 ralbii ⊢ ∀ z ∈ Base K z ≤ K x ↔ ∀ z ∈ Base K ∀ y ∈ ∅ z ≤ K y → z ≤ K x
14 ral0 ⊢ ∀ y ∈ ∅ x ≤ K y
15 14 biantrur ⊢ ∀ z ∈ Base K ∀ y ∈ ∅ z ≤ K y → z ≤ K x ↔ ∀ y ∈ ∅ x ≤ K y ∧ ∀ z ∈ Base K ∀ y ∈ ∅ z ≤ K y → z ≤ K x
16 13 15 bitri ⊢ ∀ z ∈ Base K z ≤ K x ↔ ∀ y ∈ ∅ x ≤ K y ∧ ∀ z ∈ Base K ∀ y ∈ ∅ z ≤ K y → z ≤ K x
17 10 adantr ⊢ K ∈ OP ∧ x ∈ Base K → 1 ˙ ∈ Base K
18 breq1 ⊢ z = 1 ˙ → z ≤ K x ↔ 1 ˙ ≤ K x
19 18 rspcv ⊢ 1 ˙ ∈ Base K → ∀ z ∈ Base K z ≤ K x → 1 ˙ ≤ K x
20 17 19 syl ⊢ K ∈ OP ∧ x ∈ Base K → ∀ z ∈ Base K z ≤ K x → 1 ˙ ≤ K x
21 3 4 2 op1le ⊢ K ∈ OP ∧ x ∈ Base K → 1 ˙ ≤ K x ↔ x = 1 ˙
22 20 21 sylibd ⊢ K ∈ OP ∧ x ∈ Base K → ∀ z ∈ Base K z ≤ K x → x = 1 ˙
23 3 4 2 ople1 ⊢ K ∈ OP ∧ z ∈ Base K → z ≤ K 1 ˙
24 23 adantlr ⊢ K ∈ OP ∧ x ∈ Base K ∧ z ∈ Base K → z ≤ K 1 ˙
25 24 ex ⊢ K ∈ OP ∧ x ∈ Base K → z ∈ Base K → z ≤ K 1 ˙
26 breq2 ⊢ x = 1 ˙ → z ≤ K x ↔ z ≤ K 1 ˙
27 26 biimprcd ⊢ z ≤ K 1 ˙ → x = 1 ˙ → z ≤ K x
28 25 27 syl6 ⊢ K ∈ OP ∧ x ∈ Base K → z ∈ Base K → x = 1 ˙ → z ≤ K x
29 28 com23 ⊢ K ∈ OP ∧ x ∈ Base K → x = 1 ˙ → z ∈ Base K → z ≤ K x
30 29 ralrimdv ⊢ K ∈ OP ∧ x ∈ Base K → x = 1 ˙ → ∀ z ∈ Base K z ≤ K x
31 22 30 impbid ⊢ K ∈ OP ∧ x ∈ Base K → ∀ z ∈ Base K z ≤ K x ↔ x = 1 ˙
32 16 31 bitr3id ⊢ K ∈ OP ∧ x ∈ Base K → ∀ y ∈ ∅ x ≤ K y ∧ ∀ z ∈ Base K ∀ y ∈ ∅ z ≤ K y → z ≤ K x ↔ x = 1 ˙
33 10 32 riota5 ⊢ K ∈ OP → ι x ∈ Base K | ∀ y ∈ ∅ x ≤ K y ∧ ∀ z ∈ Base K ∀ y ∈ ∅ z ≤ K y → z ≤ K x = 1 ˙
34 9 33 eqtrd ⊢ K ∈ OP → G ⁡ ∅ = 1 ˙