Metamath Proof Explorer


Theorem lubprop

Description: Properties of greatest lower bound of a poset. (Contributed by NM, 22-Oct-2011) (Revised by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubprop.b 𝐵 = ( Base ‘ 𝐾 )
lubprop.l = ( le ‘ 𝐾 )
lubprop.u 𝑈 = ( lub ‘ 𝐾 )
lubprop.k ( 𝜑𝐾𝑉 )
lubprop.s ( 𝜑𝑆 ∈ dom 𝑈 )
Assertion lubprop ( 𝜑 → ( ∀ 𝑦𝑆 𝑦 ( 𝑈𝑆 ) ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧 → ( 𝑈𝑆 ) 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 lubprop.b 𝐵 = ( Base ‘ 𝐾 )
2 lubprop.l = ( le ‘ 𝐾 )
3 lubprop.u 𝑈 = ( lub ‘ 𝐾 )
4 lubprop.k ( 𝜑𝐾𝑉 )
5 lubprop.s ( 𝜑𝑆 ∈ dom 𝑈 )
6 biid ( ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) ↔ ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) )
7 1 2 3 4 5 lubelss ( 𝜑𝑆𝐵 )
8 1 2 3 6 4 7 lubval ( 𝜑 → ( 𝑈𝑆 ) = ( 𝑥𝐵 ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) ) )
9 8 eqcomd ( 𝜑 → ( 𝑥𝐵 ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) ) = ( 𝑈𝑆 ) )
10 1 3 4 5 lubcl ( 𝜑 → ( 𝑈𝑆 ) ∈ 𝐵 )
11 1 2 3 6 4 5 lubeu ( 𝜑 → ∃! 𝑥𝐵 ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) )
12 breq2 ( 𝑥 = ( 𝑈𝑆 ) → ( 𝑦 𝑥𝑦 ( 𝑈𝑆 ) ) )
13 12 ralbidv ( 𝑥 = ( 𝑈𝑆 ) → ( ∀ 𝑦𝑆 𝑦 𝑥 ↔ ∀ 𝑦𝑆 𝑦 ( 𝑈𝑆 ) ) )
14 breq1 ( 𝑥 = ( 𝑈𝑆 ) → ( 𝑥 𝑧 ↔ ( 𝑈𝑆 ) 𝑧 ) )
15 14 imbi2d ( 𝑥 = ( 𝑈𝑆 ) → ( ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ↔ ( ∀ 𝑦𝑆 𝑦 𝑧 → ( 𝑈𝑆 ) 𝑧 ) ) )
16 15 ralbidv ( 𝑥 = ( 𝑈𝑆 ) → ( ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ↔ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧 → ( 𝑈𝑆 ) 𝑧 ) ) )
17 13 16 anbi12d ( 𝑥 = ( 𝑈𝑆 ) → ( ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) ↔ ( ∀ 𝑦𝑆 𝑦 ( 𝑈𝑆 ) ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧 → ( 𝑈𝑆 ) 𝑧 ) ) ) )
18 17 riota2 ( ( ( 𝑈𝑆 ) ∈ 𝐵 ∧ ∃! 𝑥𝐵 ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) ) → ( ( ∀ 𝑦𝑆 𝑦 ( 𝑈𝑆 ) ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧 → ( 𝑈𝑆 ) 𝑧 ) ) ↔ ( 𝑥𝐵 ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) ) = ( 𝑈𝑆 ) ) )
19 10 11 18 syl2anc ( 𝜑 → ( ( ∀ 𝑦𝑆 𝑦 ( 𝑈𝑆 ) ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧 → ( 𝑈𝑆 ) 𝑧 ) ) ↔ ( 𝑥𝐵 ( ∀ 𝑦𝑆 𝑦 𝑥 ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧𝑥 𝑧 ) ) ) = ( 𝑈𝑆 ) ) )
20 9 19 mpbird ( 𝜑 → ( ∀ 𝑦𝑆 𝑦 ( 𝑈𝑆 ) ∧ ∀ 𝑧𝐵 ( ∀ 𝑦𝑆 𝑦 𝑧 → ( 𝑈𝑆 ) 𝑧 ) ) )