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 ) = 𝑁 ) )