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