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 ⊢ G = glb ⁡ K
meetfval.m ⊢ ∧ ˙ = meet ⁡ K
Assertion meetfval2 ⊢ K ∈ V → ∧ ˙ = x y z | x y ∈ dom ⁡ G ∧ z = G ⁡ x y

Proof

Step Hyp Ref Expression
1 meetfval.u ⊢ G = glb ⁡ K
2 meetfval.m ⊢ ∧ ˙ = meet ⁡ K
3 1 2 meetfval ⊢ K ∈ V → ∧ ˙ = x y z | x y G z
4 1 glbfun ⊢ Fun ⁡ G
5 funbrfv2b ⊢ Fun ⁡ G → x y G z ↔ x y ∈ dom ⁡ G ∧ G ⁡ x y = z
6 4 5 ax-mp ⊢ x y G z ↔ x y ∈ dom ⁡ G ∧ G ⁡ x y = z
7 eqcom ⊢ G ⁡ x y = z ↔ z = G ⁡ x y
8 7 anbi2i ⊢ x y ∈ dom ⁡ G ∧ G ⁡ x y = z ↔ x y ∈ dom ⁡ G ∧ z = G ⁡ x y
9 6 8 bitri ⊢ x y G z ↔ x y ∈ dom ⁡ G ∧ z = G ⁡ x y
10 9 oprabbii ⊢ x y z | x y G z = x y z | x y ∈ dom ⁡ G ∧ z = G ⁡ x y
11 3 10 eqtrdi ⊢ K ∈ V → ∧ ˙ = x y z | x y ∈ dom ⁡ G ∧ z = G ⁡ x y