Theorem glbdm

Description: Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		glbfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		glbfval.l	⊢ ≤ = ( le ‘ 𝐾 )
3		glbfval.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		glbfval.p	⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
5		glbfval.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
6	1 2 3 4 5	glbfval	⊢ ( 𝜑 → 𝐺 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) )
7	6	dmeqd	⊢ ( 𝜑 → dom 𝐺 = dom ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) )
8		riotaex	⊢ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ∈ V
9		eqid	⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
10	8 9	dmmpti	⊢ dom ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) = 𝒫 𝐵
11	10	ineq2i	⊢ ( { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ∩ dom ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ) = ( { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ∩ 𝒫 𝐵 )
12		dmres	⊢ dom ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) = ( { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ∩ dom ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) )
13		dfrab2	⊢ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } = ( { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ∩ 𝒫 𝐵 )
14	11 12 13	3eqtr4i	⊢ dom ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 }
15	7 14	eqtrdi	⊢ ( 𝜑 → dom 𝐺 = { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } )