efgval

Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Hypotheses	efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
Assertion	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⟩ ”⟩⟩))\}$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		vex	$⊢ i \in V$
4		2on	$⊢ 2_{𝑜} \in On$
5	4	elexi	$⊢ 2_{𝑜} \in V$
6	3 5	xpex	$⊢ i \times 2_{𝑜} \in V$
7		wrdexg	$⊢ i \times 2_{𝑜} \in V \to Word (i \times 2_{𝑜}) \in V$
8		fvi	$⊢ Word (i \times 2_{𝑜}) \in V \to I (Word (i \times 2_{𝑜})) = Word (i \times 2_{𝑜})$
9	6 7 8	mp2b	$⊢ I (Word (i \times 2_{𝑜})) = Word (i \times 2_{𝑜})$
10		xpeq1	$⊢ i = I \to i \times 2_{𝑜} = I \times 2_{𝑜}$
11		wrdeq	$⊢ i \times 2_{𝑜} = I \times 2_{𝑜} \to Word (i \times 2_{𝑜}) = Word (I \times 2_{𝑜})$
12	10 11	syl	$⊢ i = I \to Word (i \times 2_{𝑜}) = Word (I \times 2_{𝑜})$
13	12	fveq2d	$⊢ i = I \to I (Word (i \times 2_{𝑜})) = I (Word (I \times 2_{𝑜}))$
14	9 13	eqtr3id	$⊢ i = I \to Word (i \times 2_{𝑜}) = I (Word (I \times 2_{𝑜}))$
15	14 1	eqtr4di	$⊢ i = I \to Word (i \times 2_{𝑜}) = W$
16		ereq2	$⊢ Word (i \times 2_{𝑜}) = W \to (r Er Word (i \times 2_{𝑜}) \leftrightarrow r Er W)$
17	15 16	syl	$⊢ i = I \to (r Er Word (i \times 2_{𝑜}) \leftrightarrow r Er W)$
18		raleq	$⊢ i = I \to (\forall y \in i \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩) \leftrightarrow \forall y \in I \forall z \in 2_{𝑜} x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))$
19	18	ralbidv	$⊢ i = I \to (\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⟩ ”⟩⟩) \leftrightarrow \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⟩ ”⟩⟩))$
20	15 19	raleqbidv	$⊢ i = I \to (\forall x \in Word (i \times 2_{𝑜}) \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⟩ ”⟩⟩) \leftrightarrow \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⟩ ”⟩⟩))$
21	17 20	anbi12d	$⊢ i = I \to ((r Er Word (i \times 2_{𝑜}) \land \forall x \in Word (i \times 2_{𝑜}) \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⟩ ”⟩⟩)) \leftrightarrow (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⟩ ”⟩⟩)))$
22	21	abbidv	$⊢ i = I \to \{r \| (r Er Word (i \times 2_{𝑜}) \land \forall x \in Word (i \times 2_{𝑜}) \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⟩ ”⟩⟩))\} = \{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⟩ ”⟩⟩))\}$
23	22	inteqd	$⊢ i = I \to ⋂ \{r \| (r Er Word (i \times 2_{𝑜}) \land \forall x \in Word (i \times 2_{𝑜}) \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⟩ ”⟩⟩))\} = ⋂ \{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⟩ ”⟩⟩))\}$
24		df-efg	$⊢ ~_{FG} = (i \in V ⟼ ⋂ \{r \| (r Er Word (i \times 2_{𝑜}) \land \forall x \in Word (i \times 2_{𝑜}) \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⟩ ”⟩⟩))\})$
25	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⟩ ”⟩⟩))$
26		intexab	$⊢ \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⟩ ”⟩⟩)) \leftrightarrow ⋂ \{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⟩ ”⟩⟩))\} \in V$
27	25 26	mpbi	$⊢ ⋂ \{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⟩ ”⟩⟩))\} \in V$
28	23 24 27	fvmpt	$⊢ I \in V \to ~_{FG} (I) = ⋂ \{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⟩ ”⟩⟩))\}$
29		fvprc	$⊢ \neg I \in V \to ~_{FG} (I) = \emptyset$
30		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⟩ ”⟩⟩))$
31	25 30	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$
32		intssuni	$⊢ \{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 \to ⋂ \{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⟩ ”⟩⟩))\} \subseteq ⋃ \{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⟩ ”⟩⟩))\}$
33	31 32	ax-mp	$⊢ ⋂ \{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⟩ ”⟩⟩))\} \subseteq ⋃ \{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⟩ ”⟩⟩))\}$
34		erssxp	$⊢ r Er W \to r \subseteq W \times W$
35	1	efgrcl	$⊢ x \in W \to (I \in V \land W = Word (I \times 2_{𝑜}))$
36	35	simpld	$⊢ x \in W \to I \in V$
37	36	con3i	$⊢ \neg I \in V \to \neg x \in W$
38	37	eq0rdv	$⊢ \neg I \in V \to W = \emptyset$
39	38	xpeq2d	$⊢ \neg I \in V \to W \times W = W \times \emptyset$
40		xp0	$⊢ W \times \emptyset = \emptyset$
41	39 40	eqtrdi	$⊢ \neg I \in V \to W \times W = \emptyset$
42		ss0b	$⊢ W \times W \subseteq \emptyset \leftrightarrow W \times W = \emptyset$
43	41 42	sylibr	$⊢ \neg I \in V \to W \times W \subseteq \emptyset$
44	34 43	sylan9ssr	$⊢ (\neg I \in V \land r Er W) \to r \subseteq \emptyset$
45	44	ex	$⊢ \neg I \in V \to (r Er W \to r \subseteq \emptyset)$
46	45	adantrd	$⊢ \neg I \in V \to ((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 \subseteq \emptyset)$
47	46	alrimiv	$⊢ \neg I \in V \to \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 \subseteq \emptyset)$
48		sseq1	$⊢ w = r \to (w \subseteq \emptyset \leftrightarrow r \subseteq \emptyset)$
49	48	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 \subseteq \emptyset \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 \subseteq \emptyset)$
50	47 49	sylibr	$⊢ \neg I \in V \to \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 \subseteq \emptyset$
51		unissb	$⊢ ⋃ \{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⟩ ”⟩⟩))\} \subseteq \emptyset \leftrightarrow \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 \subseteq \emptyset$
52	50 51	sylibr	$⊢ \neg I \in V \to ⋃ \{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⟩ ”⟩⟩))\} \subseteq \emptyset$
53	33 52	sstrid	$⊢ \neg I \in V \to ⋂ \{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⟩ ”⟩⟩))\} \subseteq \emptyset$
54		ss0	$⊢ ⋂ \{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⟩ ”⟩⟩))\} \subseteq \emptyset \to ⋂ \{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⟩ ”⟩⟩))\} = \emptyset$
55	53 54	syl	$⊢ \neg I \in V \to ⋂ \{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⟩ ”⟩⟩))\} = \emptyset$
56	29 55	eqtr4d	$⊢ \neg I \in V \to ~_{FG} (I) = ⋂ \{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⟩ ”⟩⟩))\}$
57	28 56	pm2.61i	$⊢ ~_{FG} (I) = ⋂ \{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⟩ ”⟩⟩))\}$
58	2 57	eqtri	$⊢ \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⟩ ”⟩⟩))\}$

Metamath Proof Explorer

Theorem efgval

Proof