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	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
Assertion	efgrcl	⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )

Proof

Step	Hyp	Ref	Expression
1		efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2		2on0	⊢ 2o ≠ ∅
3		dmxp	⊢ ( 2o ≠ ∅ → dom ( 𝐼 × 2o ) = 𝐼 )
4	2 3	ax-mp	⊢ dom ( 𝐼 × 2o ) = 𝐼
5		elfvex	⊢ ( 𝐴 ∈ ( I ‘ Word ( 𝐼 × 2o ) ) → Word ( 𝐼 × 2o ) ∈ V )
6	5 1	eleq2s	⊢ ( 𝐴 ∈ 𝑊 → Word ( 𝐼 × 2o ) ∈ V )
7		wrdexb	⊢ ( ( 𝐼 × 2o ) ∈ V ↔ Word ( 𝐼 × 2o ) ∈ V )
8	6 7	sylibr	⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 × 2o ) ∈ V )
9	8	dmexd	⊢ ( 𝐴 ∈ 𝑊 → dom ( 𝐼 × 2o ) ∈ V )
10	4 9	eqeltrrid	⊢ ( 𝐴 ∈ 𝑊 → 𝐼 ∈ V )
11		fvi	⊢ ( Word ( 𝐼 × 2o ) ∈ V → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
12	6 11	syl	⊢ ( 𝐴 ∈ 𝑊 → ( I ‘ Word ( 𝐼 × 2o ) ) = Word ( 𝐼 × 2o ) )
13	1 12	syl5eq	⊢ ( 𝐴 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
14	10 13	jca	⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )