Theorem fv1arycl

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

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

Proof

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