Theorem meetfval2

Description: Value of meet function for a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	meetfval.u	⊢ 𝐺 = ( glb ‘ 𝐾 )
	meetfval.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	meetfval2	⊢ ( 𝐾 ∈ 𝑉 → ∧ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } )

Proof

Step	Hyp	Ref	Expression
1		meetfval.u	⊢ 𝐺 = ( glb ‘ 𝐾 )
2		meetfval.m	⊢ ∧ = ( meet ‘ 𝐾 )
3	1 2	meetfval	⊢ ( 𝐾 ∈ 𝑉 → ∧ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } )
4	1	glbfun	⊢ Fun 𝐺
5		funbrfv2b	⊢ ( Fun 𝐺 → ( { 𝑥 , 𝑦 } 𝐺 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) ) )
6	4 5	ax-mp	⊢ ( { 𝑥 , 𝑦 } 𝐺 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) )
7		eqcom	⊢ ( ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ↔ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) )
8	7	anbi2i	⊢ ( ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = 𝑧 ) ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) )
9	6 8	bitri	⊢ ( { 𝑥 , 𝑦 } 𝐺 𝑧 ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) )
10	9	oprabbii	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } 𝐺 𝑧 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) }
11	3 10	eqtrdi	⊢ ( 𝐾 ∈ 𝑉 → ∧ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } )