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

Metamath Proof Explorer

Theorem 1fv

Description: A function on a singleton. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Proof shortened by AV, 18-Apr-2021)

Ref Expression
Assertion 1fv ( ( 𝑁 ∈ 𝑉 ∧ 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ) → ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 1 a1i ⊢ ( 𝑁 ∈ 𝑉 → 0 ∈ ℤ )
3 id ⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ 𝑉 )
4 2 3 fsnd ⊢ ( 𝑁 ∈ 𝑉 → { ⟨ 0 , 𝑁 ⟩ } : { 0 } ⟶ 𝑉 )
5 fvsng ⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ 𝑉 ) → ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 )
6 1 5 mpan ⊢ ( 𝑁 ∈ 𝑉 → ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 )
7 4 6 jca ⊢ ( 𝑁 ∈ 𝑉 → ( { ⟨ 0 , 𝑁 ⟩ } : { 0 } ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) )
8 7 adantr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ) → ( { ⟨ 0 , 𝑁 ⟩ } : { 0 } ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) )
9 id ⊢ ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } → 𝑃 = { ⟨ 0 , 𝑁 ⟩ } )
10 fz0sn ⊢ ( 0 ... 0 ) = { 0 }
11 10 a1i ⊢ ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } → ( 0 ... 0 ) = { 0 } )
12 9 11 feq12d ⊢ ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } → ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ↔ { ⟨ 0 , 𝑁 ⟩ } : { 0 } ⟶ 𝑉 ) )
13 fveq1 ⊢ ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } → ( 𝑃 ‘ 0 ) = ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) )
14 13 eqeq1d ⊢ ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } → ( ( 𝑃 ‘ 0 ) = 𝑁 ↔ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) )
15 12 14 anbi12d ⊢ ( 𝑃 = { ⟨ 0 , 𝑁 ⟩ } → ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) ↔ ( { ⟨ 0 , 𝑁 ⟩ } : { 0 } ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) ) )
16 15 adantl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ) → ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) ↔ ( { ⟨ 0 , 𝑁 ⟩ } : { 0 } ⟶ 𝑉 ∧ ( { ⟨ 0 , 𝑁 ⟩ } ‘ 0 ) = 𝑁 ) ) )
17 8 16 mpbird ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑃 = { ⟨ 0 , 𝑁 ⟩ } ) → ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) )