Metamath Proof Explorer


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 0 ..^ 1 = 0 ..^ 1
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 X V G : X 0 X A X G : X 0 X
5 c0ex 0 V
6 5 a1i X V G : X 0 X A X 0 V
7 simp3 X V G : X 0 X A X A X
8 6 7 fsnd X V G : X 0 X A X 0 A : 0 X
9 simp1 X V G : X 0 X A X X V
10 snex 0 V
11 10 a1i X V G : X 0 X A X 0 V
12 9 11 elmapd X V G : X 0 X A X 0 A X 0 0 A : 0 X
13 8 12 mpbird X V G : X 0 X A X 0 A X 0
14 4 13 ffvelrnd X V G : X 0 X A X G 0 A X
15 14 3exp X V G : X 0 X A X G 0 A X
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 |-