Metamath Proof Explorer

Theorem glb0N

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