Metamath Proof Explorer

Theorem fv2arycl

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

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (0 ..^2) = (0 ..^2)$
2	1	naryrcl	$⊢ G \in (2 -aryF X) \to (2 \in ℕ_{0} \land X \in V)$
3		2aryfvalel	$⊢ X \in V \to (G \in (2 -aryF X) \leftrightarrow G : X^{\{0, 1\}} ⟶ X)$
4		simp2	$⊢ (X \in V \land G : X^{\{0, 1\}} ⟶ X \land (A \in X \land B \in X)) \to G : X^{\{0, 1\}} ⟶ X$
5		c0ex	$⊢ 0 \in V$
6		1ex	$⊢ 1 \in V$
7		0ne1	$⊢ 0 \neq 1$
8	5 6 7	3pm3.2i	$⊢ (0 \in V \land 1 \in V \land 0 \neq 1)$
9	8	a1i	$⊢ (X \in V \land G : X^{\{0, 1\}} ⟶ X \land (A \in X \land B \in X)) \to (0 \in V \land 1 \in V \land 0 \neq 1)$
10		fprmappr	$⊢ (X \in V \land (0 \in V \land 1 \in V \land 0 \neq 1) \land (A \in X \land B \in X)) \to \{⟨0, A⟩, ⟨1, B⟩\} \in (X^{\{0, 1\}})$
11	9 10	syld3an2	$⊢ (X \in V \land G : X^{\{0, 1\}} ⟶ X \land (A \in X \land B \in X)) \to \{⟨0, A⟩, ⟨1, B⟩\} \in (X^{\{0, 1\}})$
12	4 11	ffvelcdmd	$⊢ (X \in V \land G : X^{\{0, 1\}} ⟶ X \land (A \in X \land B \in X)) \to G (\{⟨0, A⟩, ⟨1, B⟩\}) \in X$
13	12	3exp	$⊢ X \in V \to (G : X^{\{0, 1\}} ⟶ X \to ((A \in X \land B \in X) \to G (\{⟨0, A⟩, ⟨1, B⟩\}) \in X))$
14	3 13	sylbid	$⊢ X \in V \to (G \in (2 -aryF X) \to ((A \in X \land B \in X) \to G (\{⟨0, A⟩, ⟨1, B⟩\}) \in X))$
15	14	adantl	$⊢ (2 \in ℕ_{0} \land X \in V) \to (G \in (2 -aryF X) \to ((A \in X \land B \in X) \to G (\{⟨0, A⟩, ⟨1, B⟩\}) \in X))$
16	2 15	mpcom	$⊢ G \in (2 -aryF X) \to ((A \in X \land B \in X) \to G (\{⟨0, A⟩, ⟨1, B⟩\}) \in X)$
17	16	3impib	$⊢ (G \in (2 -aryF X) \land A \in X \land B \in X) \to G (\{⟨0, A⟩, ⟨1, B⟩\}) \in X$