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 × 2 𝑜
Assertion efgrcl ⊢ A ∈ W → I ∈ V ∧ W = Word I × 2 𝑜

Proof

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