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

Metamath Proof Explorer

Theorem p0val

Description: Value of poset zero. (Contributed by NM, 12-Oct-2011)

Ref Expression
Hypotheses p0val.b ⊢ B = Base K
p0val.g ⊢ G = glb ⁡ K
p0val.z ⊢ 0 ˙ = 0. ⁡ K
Assertion p0val ⊢ K ∈ V → 0 ˙ = G ⁡ B

Proof

Step Hyp Ref Expression
1 p0val.b ⊢ B = Base K
2 p0val.g ⊢ G = glb ⁡ K
3 p0val.z ⊢ 0 ˙ = 0. ⁡ K
4 elex ⊢ K ∈ V → K ∈ V
5 fveq2 ⊢ p = K → glb ⁡ p = glb ⁡ K
6 5 2 eqtr4di ⊢ p = K → glb ⁡ p = G
7 fveq2 ⊢ p = K → Base p = Base K
8 7 1 eqtr4di ⊢ p = K → Base p = B
9 6 8 fveq12d ⊢ p = K → glb ⁡ p ⁡ Base p = G ⁡ B
10 df-p0 ⊢ 0. = p ∈ V ⟼ glb ⁡ p ⁡ Base p
11 fvex ⊢ G ⁡ B ∈ V
12 9 10 11 fvmpt ⊢ K ∈ V → 0. ⁡ K = G ⁡ B
13 3 12 eqtrid ⊢ K ∈ V → 0 ˙ = G ⁡ B
14 4 13 syl ⊢ K ∈ V → 0 ˙ = G ⁡ B