1arympt1fv

Description: The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024)

		Ref	Expression
	Hypothesis	1arympt1.f	$⊢ F = (x \in (X^{\{0\}}) ⟼ A (x (0)))$
	Assertion	1arympt1fv	$⊢ (X \in V \land B \in X) \to F (\{⟨0, B⟩\}) = A (B)$

Proof

Step	Hyp	Ref	Expression
1		1arympt1.f	$⊢ F = (x \in (X^{\{0\}}) ⟼ A (x (0)))$
2	1	a1i	$⊢ (X \in V \land B \in X) \to F = (x \in (X^{\{0\}}) ⟼ A (x (0)))$
3		fveq1	$⊢ x = \{⟨0, B⟩\} \to x (0) = \{⟨0, B⟩\} (0)$
4	3	adantl	$⊢ ((X \in V \land B \in X) \land x = \{⟨0, B⟩\}) \to x (0) = \{⟨0, B⟩\} (0)$
5		c0ex	$⊢ 0 \in V$
6	5	a1i	$⊢ X \in V \to 0 \in V$
7	6	anim1i	$⊢ (X \in V \land B \in X) \to (0 \in V \land B \in X)$
8	7	adantr	$⊢ ((X \in V \land B \in X) \land x = \{⟨0, B⟩\}) \to (0 \in V \land B \in X)$
9		fvsng	$⊢ (0 \in V \land B \in X) \to \{⟨0, B⟩\} (0) = B$
10	8 9	syl	$⊢ ((X \in V \land B \in X) \land x = \{⟨0, B⟩\}) \to \{⟨0, B⟩\} (0) = B$
11	4 10	eqtrd	$⊢ ((X \in V \land B \in X) \land x = \{⟨0, B⟩\}) \to x (0) = B$
12	11	fveq2d	$⊢ ((X \in V \land B \in X) \land x = \{⟨0, B⟩\}) \to A (x (0)) = A (B)$
13	5	a1i	$⊢ (X \in V \land B \in X) \to 0 \in V$
14		simpr	$⊢ (X \in V \land B \in X) \to B \in X$
15	13 14	fsnd	$⊢ (X \in V \land B \in X) \to \{⟨0, B⟩\} : \{0\} ⟶ X$
16		snex	$⊢ \{0\} \in V$
17	16	a1i	$⊢ B \in X \to \{0\} \in V$
18		elmapg	$⊢ (X \in V \land \{0\} \in V) \to (\{⟨0, B⟩\} \in (X^{\{0\}}) \leftrightarrow \{⟨0, B⟩\} : \{0\} ⟶ X)$
19	17 18	sylan2	$⊢ (X \in V \land B \in X) \to (\{⟨0, B⟩\} \in (X^{\{0\}}) \leftrightarrow \{⟨0, B⟩\} : \{0\} ⟶ X)$
20	15 19	mpbird	$⊢ (X \in V \land B \in X) \to \{⟨0, B⟩\} \in (X^{\{0\}})$
21		fvexd	$⊢ (X \in V \land B \in X) \to A (B) \in V$
22	2 12 20 21	fvmptd	$⊢ (X \in V \land B \in X) \to F (\{⟨0, B⟩\}) = A (B)$

Metamath Proof Explorer

Theorem 1arympt1fv

Proof