Theorem fv1arycl

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

	Ref	Expression
Assertion	fv1arycl	|- ( ( G e. ( 1 -aryF X ) /\ A e. X ) -> ( G ` { <. 0 , A >. } ) e. X )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( 0 ..^ 1 ) = ( 0 ..^ 1 )
2	1	naryrcl	|- ( G e. ( 1 -aryF X ) -> ( 1 e. NN0 /\ X e. _V ) )
3		1aryfvalel	|- ( X e. _V -> ( G e. ( 1 -aryF X ) <-> G : ( X ^m { 0 } ) --> X ) )
4		simp2	|- ( ( X e. _V /\ G : ( X ^m { 0 } ) --> X /\ A e. X ) -> G : ( X ^m { 0 } ) --> X )
5		c0ex	|- 0 e. _V
6	5	a1i	|- ( ( X e. _V /\ G : ( X ^m { 0 } ) --> X /\ A e. X ) -> 0 e. _V )
7		simp3	|- ( ( X e. _V /\ G : ( X ^m { 0 } ) --> X /\ A e. X ) -> A e. X )
8	6 7	fsnd	|- ( ( X e. _V /\ G : ( X ^m { 0 } ) --> X /\ A e. X ) -> { <. 0 , A >. } : { 0 } --> X )
9		simp1	|- ( ( X e. _V /\ G : ( X ^m { 0 } ) --> X /\ A e. X ) -> X e. _V )
10		snex	|- { 0 } e. _V
11	10	a1i	|- ( ( X e. _V /\ G : ( X ^m { 0 } ) --> X /\ A e. X ) -> { 0 } e. _V )
12	9 11	elmapd	|- ( ( X e. _V /\ G : ( X ^m { 0 } ) --> X /\ A e. X ) -> ( { <. 0 , A >. } e. ( X ^m { 0 } ) <-> { <. 0 , A >. } : { 0 } --> X ) )
13	8 12	mpbird	|- ( ( X e. _V /\ G : ( X ^m { 0 } ) --> X /\ A e. X ) -> { <. 0 , A >. } e. ( X ^m { 0 } ) )
14	4 13	ffvelrnd	|- ( ( X e. _V /\ G : ( X ^m { 0 } ) --> X /\ A e. X ) -> ( G ` { <. 0 , A >. } ) e. X )
15	14	3exp	|- ( X e. _V -> ( G : ( X ^m { 0 } ) --> X -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) ) )
16	3 15	sylbid	|- ( X e. _V -> ( G e. ( 1 -aryF X ) -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) ) )
17	16	adantl	|- ( ( 1 e. NN0 /\ X e. _V ) -> ( G e. ( 1 -aryF X ) -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) ) )
18	2 17	mpcom	|- ( G e. ( 1 -aryF X ) -> ( A e. X -> ( G ` { <. 0 , A >. } ) e. X ) )
19	18	imp	|- ( ( G e. ( 1 -aryF X ) /\ A e. X ) -> ( G ` { <. 0 , A >. } ) e. X )