Metamath Proof Explorer


Definition df-lub

Description: Define the least upper bound (LUB) of a set of (poset) elements. The domain is restricted to exclude sets s for which the LUB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011) (Revised by NM, 6-Sep-2018)

Ref Expression
Assertion df-lub lub = ( 𝑝 ∈ V ↦ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 club lub
1 vp 𝑝
2 cvv V
3 vs 𝑠
4 cbs Base
5 1 cv 𝑝
6 5 4 cfv ( Base ‘ 𝑝 )
7 6 cpw 𝒫 ( Base ‘ 𝑝 )
8 vx 𝑥
9 vy 𝑦
10 3 cv 𝑠
11 9 cv 𝑦
12 cple le
13 5 12 cfv ( le ‘ 𝑝 )
14 8 cv 𝑥
15 11 14 13 wbr 𝑦 ( le ‘ 𝑝 ) 𝑥
16 15 9 10 wral 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥
17 vz 𝑧
18 17 cv 𝑧
19 11 18 13 wbr 𝑦 ( le ‘ 𝑝 ) 𝑧
20 19 9 10 wral 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧
21 14 18 13 wbr 𝑥 ( le ‘ 𝑝 ) 𝑧
22 20 21 wi ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 )
23 22 17 6 wral 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 )
24 16 23 wa ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) )
25 24 8 6 crio ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) )
26 3 7 25 cmpt ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) )
27 24 8 6 wreu ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) )
28 27 3 cab { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) }
29 26 28 cres ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } )
30 1 2 29 cmpt ( 𝑝 ∈ V ↦ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) )
31 0 30 wceq lub = ( 𝑝 ∈ V ↦ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) )