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 ⊢ 𝐺 = ( glb ‘ 𝐾 )
glb0.u ⊢ 1 = ( 1. ‘ 𝐾 )
Assertion glb0N ( 𝐾 ∈ OP → ( 𝐺 ‘ ∅ ) = 1 )

Proof

Step Hyp Ref Expression
1 glb0.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
2 glb0.u ⊢ 1 = ( 1. ‘ 𝐾 )
3 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 biid ⊢ ( ( ∀ 𝑦 ∈ ∅ 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ ∅ 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
6 id ⊢ ( 𝐾 ∈ OP → 𝐾 ∈ OP )
7 0ss ⊢ ∅ ⊆ ( Base ‘ 𝐾 )
8 7 a1i ⊢ ( 𝐾 ∈ OP → ∅ ⊆ ( Base ‘ 𝐾 ) )
9 3 4 1 5 6 8 glbval ⊢ ( 𝐾 ∈ OP → ( 𝐺 ‘ ∅ ) = ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) )
10 3 2 op1cl ⊢ ( 𝐾 ∈ OP → 1 ∈ ( Base ‘ 𝐾 ) )
11 ral0 ⊢ ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦
12 11 a1bi ⊢ ( 𝑧 ( le ‘ 𝐾 ) 𝑥 ↔ ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) )
13 12 ralbii ⊢ ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑧 ( le ‘ 𝐾 ) 𝑥 ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) )
14 ral0 ⊢ ∀ 𝑦 ∈ ∅ 𝑥 ( le ‘ 𝐾 ) 𝑦
15 14 biantrur ⊢ ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ↔ ( ∀ 𝑦 ∈ ∅ 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
16 13 15 bitri ⊢ ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑧 ( le ‘ 𝐾 ) 𝑥 ↔ ( ∀ 𝑦 ∈ ∅ 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
17 10 adantr ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 1 ∈ ( Base ‘ 𝐾 ) )
18 breq1 ⊢ ( 𝑧 = 1 → ( 𝑧 ( le ‘ 𝐾 ) 𝑥 ↔ 1 ( le ‘ 𝐾 ) 𝑥 ) )
19 18 rspcv ⊢ ( 1 ∈ ( Base ‘ 𝐾 ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑧 ( le ‘ 𝐾 ) 𝑥 → 1 ( le ‘ 𝐾 ) 𝑥 ) )
20 17 19 syl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑧 ( le ‘ 𝐾 ) 𝑥 → 1 ( le ‘ 𝐾 ) 𝑥 ) )
21 3 4 2 op1le ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 1 ( le ‘ 𝐾 ) 𝑥 ↔ 𝑥 = 1 ) )
22 20 21 sylibd ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑧 ( le ‘ 𝐾 ) 𝑥 → 𝑥 = 1 ) )
23 3 4 2 ople1 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → 𝑧 ( le ‘ 𝐾 ) 1 )
24 23 adantlr ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → 𝑧 ( le ‘ 𝐾 ) 1 )
25 24 ex ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐾 ) → 𝑧 ( le ‘ 𝐾 ) 1 ) )
26 breq2 ⊢ ( 𝑥 = 1 → ( 𝑧 ( le ‘ 𝐾 ) 𝑥 ↔ 𝑧 ( le ‘ 𝐾 ) 1 ) )
27 26 biimprcd ⊢ ( 𝑧 ( le ‘ 𝐾 ) 1 → ( 𝑥 = 1 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) )
28 25 27 syl6 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐾 ) → ( 𝑥 = 1 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
29 28 com23 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 = 1 → ( 𝑧 ∈ ( Base ‘ 𝐾 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
30 29 ralrimdv ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 = 1 → ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑧 ( le ‘ 𝐾 ) 𝑥 ) )
31 22 30 impbid ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑧 ( le ‘ 𝐾 ) 𝑥 ↔ 𝑥 = 1 ) )
32 16 31 bitr3id ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( ∀ 𝑦 ∈ ∅ 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ↔ 𝑥 = 1 ) )
33 10 32 riota5 ⊢ ( 𝐾 ∈ OP → ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) = 1 )
34 9 33 eqtrd ⊢ ( 𝐾 ∈ OP → ( 𝐺 ‘ ∅ ) = 1 )