Theorem p1val

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

	Ref	Expression
Hypotheses	p1val.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	p1val.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	p1val.t	⊢ 1 = ( 1. ‘ 𝐾 )
Assertion	p1val	⊢ ( 𝐾 ∈ 𝑉 → 1 = ( 𝑈 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		p1val.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		p1val.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
3		p1val.t	⊢ 1 = ( 1. ‘ 𝐾 )
4		elex	⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V )
5		fveq2	⊢ ( 𝑘 = 𝐾 → ( lub ‘ 𝑘 ) = ( lub ‘ 𝐾 ) )
6	5 2	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( lub ‘ 𝑘 ) = 𝑈 )
7		fveq2	⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
8	7 1	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
9	6 8	fveq12d	⊢ ( 𝑘 = 𝐾 → ( ( lub ‘ 𝑘 ) ‘ ( Base ‘ 𝑘 ) ) = ( 𝑈 ‘ 𝐵 ) )
10		df-p1	⊢ 1. = ( 𝑘 ∈ V ↦ ( ( lub ‘ 𝑘 ) ‘ ( Base ‘ 𝑘 ) ) )
11		fvex	⊢ ( 𝑈 ‘ 𝐵 ) ∈ V
12	9 10 11	fvmpt	⊢ ( 𝐾 ∈ V → ( 1. ‘ 𝐾 ) = ( 𝑈 ‘ 𝐵 ) )
13	3 12	syl5eq	⊢ ( 𝐾 ∈ V → 1 = ( 𝑈 ‘ 𝐵 ) )
14	4 13	syl	⊢ ( 𝐾 ∈ 𝑉 → 1 = ( 𝑈 ‘ 𝐵 ) )