glbfval

Description: Value of the greatest lower function of a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 6-Sep-2018)

	Ref	Expression
Hypotheses	glbfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	glbfval.l	⊢ ≤ = ( le ‘ 𝐾 )
	glbfval.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	glbfval.p	⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
	glbfval.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
Assertion	glbfval	⊢ ( 𝜑 → 𝐺 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) )

Proof

Step	Hyp	Ref	Expression
1		glbfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		glbfval.l	⊢ ≤ = ( le ‘ 𝐾 )
3		glbfval.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		glbfval.p	⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
5		glbfval.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
6		elex	⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V )
7		fveq2	⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) )
8	7 1	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 )
9	8	pweqd	⊢ ( 𝑝 = 𝐾 → 𝒫 ( Base ‘ 𝑝 ) = 𝒫 𝐵 )
10		fveq2	⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ( le ‘ 𝐾 ) )
11	10 2	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ≤ )
12	11	breqd	⊢ ( 𝑝 = 𝐾 → ( 𝑥 ( le ‘ 𝑝 ) 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
13	12	ralbidv	⊢ ( 𝑝 = 𝐾 → ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ↔ ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ) )
14	11	breqd	⊢ ( 𝑝 = 𝐾 → ( 𝑧 ( le ‘ 𝑝 ) 𝑦 ↔ 𝑧 ≤ 𝑦 ) )
15	14	ralbidv	⊢ ( 𝑝 = 𝐾 → ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 ↔ ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 ) )
16	11	breqd	⊢ ( 𝑝 = 𝐾 → ( 𝑧 ( le ‘ 𝑝 ) 𝑥 ↔ 𝑧 ≤ 𝑥 ) )
17	15 16	imbi12d	⊢ ( 𝑝 = 𝐾 → ( ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
18	8 17	raleqbidv	⊢ ( 𝑝 = 𝐾 → ( ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
19	13 18	anbi12d	⊢ ( 𝑝 = 𝐾 → ( ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
20	8 19	riotaeqbidv	⊢ ( 𝑝 = 𝐾 → ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) ) = ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
21	9 20	mpteq12dv	⊢ ( 𝑝 = 𝐾 → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) )
22	19	reubidv	⊢ ( 𝑝 = 𝐾 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) ↔ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
23		reueq1	⊢ ( ( Base ‘ 𝑝 ) = 𝐵 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
24	8 23	syl	⊢ ( 𝑝 = 𝐾 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
25	22 24	bitrd	⊢ ( 𝑝 = 𝐾 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
26	25	abbidv	⊢ ( 𝑝 = 𝐾 → { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) } = { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } )
27	21 26	reseq12d	⊢ ( 𝑝 = 𝐾 → ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) } ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ) )
28		df-glb	⊢ glb = ( 𝑝 ∈ V ↦ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑥 ( le ‘ 𝑝 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑧 ( le ‘ 𝑝 ) 𝑦 → 𝑧 ( le ‘ 𝑝 ) 𝑥 ) ) } ) )
29	1	fvexi	⊢ 𝐵 ∈ V
30	29	pwex	⊢ 𝒫 𝐵 ∈ V
31	30	mptex	⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ∈ V
32	31	resex	⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ) ∈ V
33	27 28 32	fvmpt	⊢ ( 𝐾 ∈ V → ( glb ‘ 𝐾 ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ) )
34	4	a1i	⊢ ( 𝑥 ∈ 𝐵 → ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
35	34	riotabiia	⊢ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
36	35	mpteq2i	⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
37	4	reubii	⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
38	37	abbii	⊢ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } = { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) }
39	36 38	reseq12i	⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } )
40	33 3 39	3eqtr4g	⊢ ( 𝐾 ∈ V → 𝐺 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) )
41	5 6 40	3syl	⊢ ( 𝜑 → 𝐺 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) )

Metamath Proof Explorer

Theorem glbfval

Proof