Theorem meetcl

Description: Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	meetcl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	meetcl.m	⊢ ∧ = ( meet ‘ 𝐾 )
	meetcl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	meetcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	meetcl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	meetcl.e	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ )
Assertion	meetcl	⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		meetcl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		meetcl.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		meetcl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
4		meetcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		meetcl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		meetcl.e	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ )
7		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
8	7 2 3 4 5	meetval	⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
9	7 2 3 4 5	meetdef	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ↔ { 𝑋 , 𝑌 } ∈ dom ( glb ‘ 𝐾 ) ) )
10	6 9	mpbid	⊢ ( 𝜑 → { 𝑋 , 𝑌 } ∈ dom ( glb ‘ 𝐾 ) )
11	1 7 3 10	glbcl	⊢ ( 𝜑 → ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) ∈ 𝐵 )
12	8 11	eqeltrd	⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )