Metamath Proof Explorer

Theorem poslubd

Description: Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses poslubd.l ⊢ ≤ = ( le ‘ 𝐾 )
poslubd.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
poslubd.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
poslubd.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
poslubd.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
poslubd.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
poslubd.ub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ≤ 𝑇 )
poslubd.le ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 ) → 𝑇 ≤ 𝑦 )
Assertion poslubd ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = 𝑇 )

Proof

Step Hyp Ref Expression
1 poslubd.l ⊢ ≤ = ( le ‘ 𝐾 )
2 poslubd.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
3 poslubd.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 poslubd.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
5 poslubd.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6 poslubd.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
7 poslubd.ub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ≤ 𝑇 )
8 poslubd.le ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 ) → 𝑇 ≤ 𝑦 )
9 biid ⊢ ( ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) )
10 2 1 3 9 4 5 lubval ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ( ℩ 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ) )
11 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑇 )
12 8 3expia ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑇 ≤ 𝑦 ) )
13 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑇 ≤ 𝑦 ) )
14 11 13 jca ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑇 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑇 ≤ 𝑦 ) ) )
15 breq2 ⊢ ( 𝑧 = 𝑇 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ≤ 𝑇 ) )
16 15 ralbidv ⊢ ( 𝑧 = 𝑇 → ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ↔ ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑇 ) )
17 breq1 ⊢ ( 𝑧 = 𝑇 → ( 𝑧 ≤ 𝑦 ↔ 𝑇 ≤ 𝑦 ) )
18 17 imbi2d ⊢ ( 𝑧 = 𝑇 → ( ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ↔ ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑇 ≤ 𝑦 ) ) )
19 18 ralbidv ⊢ ( 𝑧 = 𝑇 → ( ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑇 ≤ 𝑦 ) ) )
20 16 19 anbi12d ⊢ ( 𝑧 = 𝑇 → ( ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑇 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑇 ≤ 𝑦 ) ) ) )
21 20 rspcev ⊢ ( ( 𝑇 ∈ 𝐵 ∧ ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑇 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑇 ≤ 𝑦 ) ) ) → ∃ 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) )
22 6 14 21 syl2anc ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) )
23 1 2 poslubmo ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵 ) → ∃* 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) )
24 4 5 23 syl2anc ⊢ ( 𝜑 → ∃* 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) )
25 reu5 ⊢ ( ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ↔ ( ∃ 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ∧ ∃* 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ) )
26 22 24 25 sylanbrc ⊢ ( 𝜑 → ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) )
27 20 riota2 ⊢ ( ( 𝑇 ∈ 𝐵 ∧ ∃! 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ) → ( ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑇 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑇 ≤ 𝑦 ) ) ↔ ( ℩ 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ) = 𝑇 ) )
28 6 26 27 syl2anc ⊢ ( 𝜑 → ( ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑇 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑇 ≤ 𝑦 ) ) ↔ ( ℩ 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ) = 𝑇 ) )
29 14 28 mpbid ⊢ ( 𝜑 → ( ℩ 𝑧 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑧 ≤ 𝑦 ) ) ) = 𝑇 )
30 10 29 eqtrd ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = 𝑇 )