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	eqtrid	⊢ ( 𝐾 ∈ V → 0 = ( 𝐺 ‘ 𝐵 ) )
14	4 13	syl	⊢ ( 𝐾 ∈ 𝑉 → 0 = ( 𝐺 ‘ 𝐵 ) )