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	$⊢ (N \in V \land P = \{⟨0, N⟩\}) \to (P : (0 \dots 0) ⟶ V \land P (0) = N)$

Step	Hyp	Ref	Expression
1		0z	$⊢ 0 \in ℤ$
2	1	a1i	$⊢ N \in V \to 0 \in ℤ$
3		id	$⊢ N \in V \to N \in V$
4	2 3	fsnd	$⊢ N \in V \to \{⟨0, N⟩\} : \{0\} ⟶ V$
5		fvsng	$⊢ (0 \in ℤ \land N \in V) \to \{⟨0, N⟩\} (0) = N$
6	1 5	mpan	$⊢ N \in V \to \{⟨0, N⟩\} (0) = N$
7	4 6	jca	$⊢ N \in V \to (\{⟨0, N⟩\} : \{0\} ⟶ V \land \{⟨0, N⟩\} (0) = N)$
8	7	adantr	$⊢ (N \in V \land P = \{⟨0, N⟩\}) \to (\{⟨0, N⟩\} : \{0\} ⟶ V \land \{⟨0, N⟩\} (0) = N)$
9		id	$⊢ P = \{⟨0, N⟩\} \to P = \{⟨0, N⟩\}$
10		fz0sn	$⊢ (0 \dots 0) = \{0\}$
11	10	a1i	$⊢ P = \{⟨0, N⟩\} \to (0 \dots 0) = \{0\}$
12	9 11	feq12d	$⊢ P = \{⟨0, N⟩\} \to (P : (0 \dots 0) ⟶ V \leftrightarrow \{⟨0, N⟩\} : \{0\} ⟶ V)$
13		fveq1	$⊢ P = \{⟨0, N⟩\} \to P (0) = \{⟨0, N⟩\} (0)$
14	13	eqeq1d	$⊢ P = \{⟨0, N⟩\} \to (P (0) = N \leftrightarrow \{⟨0, N⟩\} (0) = N)$
15	12 14	anbi12d	$⊢ P = \{⟨0, N⟩\} \to ((P : (0 \dots 0) ⟶ V \land P (0) = N) \leftrightarrow (\{⟨0, N⟩\} : \{0\} ⟶ V \land \{⟨0, N⟩\} (0) = N))$
16	15	adantl	$⊢ (N \in V \land P = \{⟨0, N⟩\}) \to ((P : (0 \dots 0) ⟶ V \land P (0) = N) \leftrightarrow (\{⟨0, N⟩\} : \{0\} ⟶ V \land \{⟨0, N⟩\} (0) = N))$
17	8 16	mpbird	$⊢ (N \in V \land P = \{⟨0, N⟩\}) \to (P : (0 \dots 0) ⟶ V \land P (0) = N)$

Metamath Proof Explorer