Theorem fv2arycl

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

	Ref	Expression
Assertion	fv2arycl	Could not format assertion : No typesetting found for |- ( ( G e. ( 2 -aryF X ) /\ A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(0..^2\right)=\left(0..^2\right)$$
2	1	naryrcl	Could not format ( G e. ( 2 -aryF X ) -> ( 2 e. NN0 /\ X e. _V ) ) : No typesetting found for |- ( G e. ( 2 -aryF X ) -> ( 2 e. NN0 /\ X e. _V ) ) with typecode |-
3		2aryfvalel	Could not format ( X e. _V -> ( G e. ( 2 -aryF X ) <-> G : ( X ^m { 0 , 1 } ) --> X ) ) : No typesetting found for |- ( X e. _V -> ( G e. ( 2 -aryF X ) <-> G : ( X ^m { 0 , 1 } ) --> X ) ) with typecode |-
4		simp2	$$⊢\left(X\in \mathrm{V}\wedge G:X^{\left\{0,1\right\}}⟶X\wedge \left(A\in X\wedge B\in X\right)\right)\to G:X^{\left\{0,1\right\}}⟶X$$
5		c0ex	$$⊢0\in \mathrm{V}$$
6		1ex	$$⊢1\in \mathrm{V}$$
7		0ne1	$$⊢0\ne 1$$
8	5 6 7	3pm3.2i	$$⊢\left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\wedge 0\ne 1\right)$$
9	8	a1i	$$⊢\left(X\in \mathrm{V}\wedge G:X^{\left\{0,1\right\}}⟶X\wedge \left(A\in X\wedge B\in X\right)\right)\to \left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\wedge 0\ne 1\right)$$
10		fprmappr	$$⊢\left(X\in \mathrm{V}\wedge \left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\wedge 0\ne 1\right)\wedge \left(A\in X\wedge B\in X\right)\right)\to \left\{⟨0,A⟩,⟨1,B⟩\right\}\in \left(X^{\left\{0,1\right\}}\right)$$
11	9 10	syld3an2	$$⊢\left(X\in \mathrm{V}\wedge G:X^{\left\{0,1\right\}}⟶X\wedge \left(A\in X\wedge B\in X\right)\right)\to \left\{⟨0,A⟩,⟨1,B⟩\right\}\in \left(X^{\left\{0,1\right\}}\right)$$
12	4 11	ffvelrnd	$$⊢\left(X\in \mathrm{V}\wedge G:X^{\left\{0,1\right\}}⟶X\wedge \left(A\in X\wedge B\in X\right)\right)\to G\left(\left\{⟨0,A⟩,⟨1,B⟩\right\}\right)\in X$$
13	12	3exp	$$⊢X\in \mathrm{V}\to \left(G:X^{\left\{0,1\right\}}⟶X\to \left(\left(A\in X\wedge B\in X\right)\to G\left(\left\{⟨0,A⟩,⟨1,B⟩\right\}\right)\in X\right)\right)$$
14	3 13	sylbid	Could not format ( X e. _V -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) ) : No typesetting found for |- ( X e. _V -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) ) with typecode |-
15	14	adantl	Could not format ( ( 2 e. NN0 /\ X e. _V ) -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) ) : No typesetting found for |- ( ( 2 e. NN0 /\ X e. _V ) -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) ) with typecode |-
16	2 15	mpcom	Could not format ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) : No typesetting found for |- ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) with typecode |-
17	16	3impib	Could not format ( ( G e. ( 2 -aryF X ) /\ A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) : No typesetting found for |- ( ( G e. ( 2 -aryF X ) /\ A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) with typecode |-