Metamath Proof Explorer

Theorem efger

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

		Ref	Expression
	Hypotheses	efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	Assertion	efger	$⊢ \underset{˙}{\sim} Er W$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3	1	efglem	$⊢ \exists r (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))$
4		abn0	$⊢ \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\} \neq \emptyset \leftrightarrow \exists r (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))$
5	3 4	mpbir	$⊢ \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\} \neq \emptyset$
6		ereq1	$⊢ w = r \to (w Er W \leftrightarrow r Er W)$
7	6	ralab2	$⊢ \forall w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\} w Er W \leftrightarrow \forall r ((r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩)) \to r Er W)$
8		simpl	$⊢ (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩)) \to r Er W$
9	7 8	mpgbir	$⊢ \forall w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\} w Er W$
10		iiner	$⊢ (\{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\} \neq \emptyset \land \forall w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\} w Er W) \to ⋂_{w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\}} w Er W$
11	5 9 10	mp2an	$⊢ ⋂_{w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\}} w Er W$
12	1 2	efgval	$⊢ \underset{˙}{\sim} = ⋂ \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\}$
13		intiin	$⊢ ⋂ \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\} = ⋂_{w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\}} w$
14	12 13	eqtri	$⊢ \underset{˙}{\sim} = ⋂_{w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\}} w$
15		ereq1	$⊢ \underset{˙}{\sim} = ⋂_{w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\}} w \to (\underset{˙}{\sim} Er W \leftrightarrow ⋂_{w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\}} w Er W)$
16	14 15	ax-mp	$⊢ \underset{˙}{\sim} Er W \leftrightarrow ⋂_{w \in \{r \| (r Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))\}} w Er W$
17	11 16	mpbir	$⊢ \underset{˙}{\sim} Er W$