This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )