This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑝 ) 𝑧 ) ) } ) )