Definition df-glb

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cglb	⊢ glb
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	8	cv	⊢ 𝑥
12		cple	⊢ le
13	5 12	cfv	⊢ ( le ‘ 𝑝 )
14	9	cv	⊢ 𝑦
15	11 14 13	wbr	⊢ 𝑥 ( le ‘ 𝑝 ) 𝑦
16	15 9 10	wral	⊢ ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦
17		vz	⊢ 𝑧
18	17	cv	⊢ 𝑧
19	18 14 13	wbr	⊢ 𝑧 ( le ‘ 𝑝 ) 𝑦
20	19 9 10	wral	⊢ ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦
21	18 11 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	⊢ glb = ( 𝑝 ∈ V ↦ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) } ) )