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

Metamath Proof Explorer

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