This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } )