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 ⊢ 𝑊 = ( 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 eqtrid ⊢ ( 𝐴 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
14 10 13 jca ⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )