glbval

Description: Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying S e. dom U ) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	glbval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	glbval.l	⊢ ≤ = ( le ‘ 𝐾 )
	glbval.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	glbval.p	⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
	glbva.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	glbval.ss	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion	glbval	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		glbval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		glbval.l	⊢ ≤ = ( le ‘ 𝐾 )
3		glbval.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		glbval.p	⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
5		glbva.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
6		glbval.ss	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
7		biid	⊢ ( ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
8	5	adantr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → 𝐾 ∈ 𝑉 )
9	1 2 3 7 8	glbfval	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → 𝐺 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ) )
10	9	fveq1d	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑆 ) = ( ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ) ‘ 𝑆 ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → 𝑆 ∈ dom 𝐺 )
12	1 2 3 4 8 11	glbeu	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → ∃! 𝑥 ∈ 𝐵 𝜓 )
13		raleq	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) )
14		raleq	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 ) )
15	14	imbi1d	⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
16	15	ralbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
17	13 16	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
18	17 4	bitr4di	⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ 𝜓 ) )
19	18	reubidv	⊢ ( 𝑠 = 𝑆 → ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
20	11 12 19	elabd	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → 𝑆 ∈ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } )
21	20	fvresd	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → ( ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ) ‘ 𝑆 ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ‘ 𝑆 ) )
22	6	adantr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → 𝑆 ⊆ 𝐵 )
23	1	fvexi	⊢ 𝐵 ∈ V
24	23	elpw2	⊢ ( 𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵 )
25	22 24	sylibr	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → 𝑆 ∈ 𝒫 𝐵 )
26	18	riotabidv	⊢ ( 𝑠 = 𝑆 → ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
27		eqid	⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
28		riotaex	⊢ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ∈ V
29	26 27 28	fvmpt	⊢ ( 𝑆 ∈ 𝒫 𝐵 → ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
30	25 29	syl	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
31	10 21 30	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑆 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
32		ndmfv	⊢ ( ¬ 𝑆 ∈ dom 𝐺 → ( 𝐺 ‘ 𝑆 ) = ∅ )
33	32	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑆 ) = ∅ )
34	1 2 3 4 5	glbeldm	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) )
35	34	biimprd	⊢ ( 𝜑 → ( ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) → 𝑆 ∈ dom 𝐺 ) )
36	6 35	mpand	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 → 𝑆 ∈ dom 𝐺 ) )
37	36	con3dimp	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺 ) → ¬ ∃! 𝑥 ∈ 𝐵 𝜓 )
38		riotaund	⊢ ( ¬ ∃! 𝑥 ∈ 𝐵 𝜓 → ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ∅ )
39	37 38	syl	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺 ) → ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ∅ )
40	33 39	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝑆 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
41	31 40	pm2.61dan	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )

Metamath Proof Explorer

Theorem glbval

Proof