Theorem efgrcl

Description: Lemma for efgval . (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypothesis	efgval.w	|- W = ( _I ` Word ( I X. 2o ) )
Assertion	efgrcl	|- ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )

Proof

Step	Hyp	Ref	Expression
1		efgval.w	|- W = ( _I ` Word ( I X. 2o ) )
2		2on0	|- 2o =/= (/)
3		dmxp	|- ( 2o =/= (/) -> dom ( I X. 2o ) = I )
4	2 3	ax-mp	|- dom ( I X. 2o ) = I
5		elfvex	|- ( A e. ( _I ` Word ( I X. 2o ) ) -> Word ( I X. 2o ) e. _V )
6	5 1	eleq2s	|- ( A e. W -> Word ( I X. 2o ) e. _V )
7		wrdexb	|- ( ( I X. 2o ) e. _V <-> Word ( I X. 2o ) e. _V )
8	6 7	sylibr	|- ( A e. W -> ( I X. 2o ) e. _V )
9	8	dmexd	|- ( A e. W -> dom ( I X. 2o ) e. _V )
10	4 9	eqeltrrid	|- ( A e. W -> I e. _V )
11		fvi	|- ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
12	6 11	syl	|- ( A e. W -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
13	1 12	eqtrid	|- ( A e. W -> W = Word ( I X. 2o ) )
14	10 13	jca	|- ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )