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 ‘ 𝐾 )
lub0.z ⊢ 0 = ( 0. ‘ 𝐾 )
Assertion lub0N ( 𝐾 ∈ OP → ( 1 ‘ ∅ ) = 0 )

Proof

Step Hyp Ref Expression
1 lub0.u ⊢ 1 = ( lub ‘ 𝐾 )
2 lub0.z ⊢ 0 = ( 0. ‘ 𝐾 )
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 lubval ⊢ ( 𝐾 ∈ OP → ( 1 ‘ ∅ ) = ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
10 3 2 op0cl ⊢ ( 𝐾 ∈ OP → 0 ∈ ( 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 ‘ 𝐾 ) ) → 0 ∈ ( Base ‘ 𝐾 ) )
18 breq2 ⊢ ( 𝑧 = 0 → ( 𝑥 ( le ‘ 𝐾 ) 𝑧 ↔ 𝑥 ( le ‘ 𝐾 ) 0 ) )
19 18 rspcv ⊢ ( 0 ∈ ( Base ‘ 𝐾 ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑥 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 0 ) )
20 17 19 syl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑥 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 0 ) )
21 3 4 2 ople0 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( le ‘ 𝐾 ) 0 ↔ 𝑥 = 0 ) )
22 20 21 sylibd ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑥 ( le ‘ 𝐾 ) 𝑧 → 𝑥 = 0 ) )
23 3 4 2 op0le ⊢ ( ( 𝐾 ∈ OP ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑧 )
24 23 adantlr ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑧 )
25 24 ex ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐾 ) → 0 ( le ‘ 𝐾 ) 𝑧 ) )
26 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ( le ‘ 𝐾 ) 𝑧 ↔ 0 ( le ‘ 𝐾 ) 𝑧 ) )
27 26 biimprcd ⊢ ( 0 ( le ‘ 𝐾 ) 𝑧 → ( 𝑥 = 0 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) )
28 25 27 syl6 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐾 ) → ( 𝑥 = 0 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
29 28 com23 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 = 0 → ( 𝑧 ∈ ( Base ‘ 𝐾 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
30 29 ralrimdv ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 = 0 → ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑥 ( le ‘ 𝐾 ) 𝑧 ) )
31 22 30 impbid ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) 𝑥 ( le ‘ 𝐾 ) 𝑧 ↔ 𝑥 = 0 ) )
32 16 31 bitr3id ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ 𝑥 = 0 ) )
33 10 32 riota5 ⊢ ( 𝐾 ∈ OP → ( ℩ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ ∅ 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) = 0 )
34 9 33 eqtrd ⊢ ( 𝐾 ∈ OP → ( 1 ‘ ∅ ) = 0 )