Metamath Proof Explorer

Theorem fv1arycl

Description: Closure of a unary (endo)function. (Contributed by AV, 18-May-2024)

		Ref	Expression
	Assertion	fv1arycl	$⊢ (G \in (1 -aryF X) \land A \in X) \to G (\{⟨0, A⟩\}) \in X$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (0 ..^1) = (0 ..^1)$
2	1	naryrcl	$⊢ G \in (1 -aryF X) \to (1 \in ℕ_{0} \land X \in V)$
3		1aryfvalel	$⊢ X \in V \to (G \in (1 -aryF X) \leftrightarrow G : X^{\{0\}} ⟶ X)$
4		simp2	$⊢ (X \in V \land G : X^{\{0\}} ⟶ X \land A \in X) \to G : X^{\{0\}} ⟶ X$
5		c0ex	$⊢ 0 \in V$
6	5	a1i	$⊢ (X \in V \land G : X^{\{0\}} ⟶ X \land A \in X) \to 0 \in V$
7		simp3	$⊢ (X \in V \land G : X^{\{0\}} ⟶ X \land A \in X) \to A \in X$
8	6 7	fsnd	$⊢ (X \in V \land G : X^{\{0\}} ⟶ X \land A \in X) \to \{⟨0, A⟩\} : \{0\} ⟶ X$
9		simp1	$⊢ (X \in V \land G : X^{\{0\}} ⟶ X \land A \in X) \to X \in V$
10		snex	$⊢ \{0\} \in V$
11	10	a1i	$⊢ (X \in V \land G : X^{\{0\}} ⟶ X \land A \in X) \to \{0\} \in V$
12	9 11	elmapd	$⊢ (X \in V \land G : X^{\{0\}} ⟶ X \land A \in X) \to (\{⟨0, A⟩\} \in (X^{\{0\}}) \leftrightarrow \{⟨0, A⟩\} : \{0\} ⟶ X)$
13	8 12	mpbird	$⊢ (X \in V \land G : X^{\{0\}} ⟶ X \land A \in X) \to \{⟨0, A⟩\} \in (X^{\{0\}})$
14	4 13	ffvelcdmd	$⊢ (X \in V \land G : X^{\{0\}} ⟶ X \land A \in X) \to G (\{⟨0, A⟩\}) \in X$
15	14	3exp	$⊢ X \in V \to (G : X^{\{0\}} ⟶ X \to (A \in X \to G (\{⟨0, A⟩\}) \in X))$
16	3 15	sylbid	$⊢ X \in V \to (G \in (1 -aryF X) \to (A \in X \to G (\{⟨0, A⟩\}) \in X))$
17	16	adantl	$⊢ (1 \in ℕ_{0} \land X \in V) \to (G \in (1 -aryF X) \to (A \in X \to G (\{⟨0, A⟩\}) \in X))$
18	2 17	mpcom	$⊢ G \in (1 -aryF X) \to (A \in X \to G (\{⟨0, A⟩\}) \in X)$
19	18	imp	$⊢ (G \in (1 -aryF X) \land A \in X) \to G (\{⟨0, A⟩\}) \in X$