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=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
Assertion	efgrcl	$$⊢A\in W\to \left(I\in \mathrm{V}\wedge W=\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$$⊢W=\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$
2		2on0	$$⊢2_{𝑜}\ne \varnothing$$
3		dmxp	$$⊢2_{𝑜}\ne \varnothing \to \mathrm{dom}\left(I\times 2_{𝑜}\right)=I$$
4	2 3	ax-mp	$$⊢\mathrm{dom}\left(I\times 2_{𝑜}\right)=I$$
5		elfvex	$$⊢A\in \mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)\to \mathrm{Word}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
6	5 1	eleq2s	$$⊢A\in W\to \mathrm{Word}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
7		wrdexb	$$⊢I\times 2_{𝑜}\in \mathrm{V}\leftrightarrow \mathrm{Word}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
8	6 7	sylibr	$$⊢A\in W\to I\times 2_{𝑜}\in \mathrm{V}$$
9	8	dmexd	$$⊢A\in W\to \mathrm{dom}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
10	4 9	eqeltrrid	$$⊢A\in W\to I\in \mathrm{V}$$
11		fvi	$$⊢\mathrm{Word}\left(I\times 2_{𝑜}\right)\in \mathrm{V}\to \mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
12	6 11	syl	$$⊢A\in W\to \mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
13	1 12	eqtrid	$$⊢A\in W\to W=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
14	10 13	jca	$$⊢A\in W\to \left(I\in \mathrm{V}\wedge W=\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)$$