Metamath Proof Explorer


Theorem p0val

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

Ref Expression
Hypotheses p0val.b 𝐵 = ( Base ‘ 𝐾 )
p0val.g 𝐺 = ( glb ‘ 𝐾 )
p0val.z 0 = ( 0. ‘ 𝐾 )
Assertion p0val ( 𝐾𝑉0 = ( 𝐺𝐵 ) )

Proof

Step Hyp Ref Expression
1 p0val.b 𝐵 = ( Base ‘ 𝐾 )
2 p0val.g 𝐺 = ( glb ‘ 𝐾 )
3 p0val.z 0 = ( 0. ‘ 𝐾 )
4 elex ( 𝐾𝑉𝐾 ∈ V )
5 fveq2 ( 𝑝 = 𝐾 → ( glb ‘ 𝑝 ) = ( glb ‘ 𝐾 ) )
6 5 2 eqtr4di ( 𝑝 = 𝐾 → ( glb ‘ 𝑝 ) = 𝐺 )
7 fveq2 ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) )
8 7 1 eqtr4di ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 )
9 6 8 fveq12d ( 𝑝 = 𝐾 → ( ( glb ‘ 𝑝 ) ‘ ( Base ‘ 𝑝 ) ) = ( 𝐺𝐵 ) )
10 df-p0 0. = ( 𝑝 ∈ V ↦ ( ( glb ‘ 𝑝 ) ‘ ( Base ‘ 𝑝 ) ) )
11 fvex ( 𝐺𝐵 ) ∈ V
12 9 10 11 fvmpt ( 𝐾 ∈ V → ( 0. ‘ 𝐾 ) = ( 𝐺𝐵 ) )
13 3 12 syl5eq ( 𝐾 ∈ V → 0 = ( 𝐺𝐵 ) )
14 4 13 syl ( 𝐾𝑉0 = ( 𝐺𝐵 ) )