efglem

		Ref	Expression
	Hypothesis	efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	Assertion	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⟩ ”⟩⟩))$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		xpider	$⊢ (W \times W) Er W$
3		simpll	$⊢ ((x \in W \land n \in (0 \dots \|x\|)) \land (y \in I \land z \in 2_{𝑜})) \to x \in W$
4		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
5	1 4	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
6	5 3	sseldi	$⊢ ((x \in W \land n \in (0 \dots \|x\|)) \land (y \in I \land z \in 2_{𝑜})) \to x \in Word (I \times 2_{𝑜})$
7		opelxpi	$⊢ (y \in I \land z \in 2_{𝑜}) \to ⟨y, z⟩ \in (I \times 2_{𝑜})$
8	7	adantl	$⊢ ((x \in W \land n \in (0 \dots \|x\|)) \land (y \in I \land z \in 2_{𝑜})) \to ⟨y, z⟩ \in (I \times 2_{𝑜})$
9		2oconcl	$⊢ z \in 2_{𝑜} \to 1_{𝑜} ∖ z \in 2_{𝑜}$
10		opelxpi	$⊢ (y \in I \land 1_{𝑜} ∖ z \in 2_{𝑜}) \to ⟨y, 1_{𝑜} ∖ z⟩ \in (I \times 2_{𝑜})$
11	9 10	sylan2	$⊢ (y \in I \land z \in 2_{𝑜}) \to ⟨y, 1_{𝑜} ∖ z⟩ \in (I \times 2_{𝑜})$
12	11	adantl	$⊢ ((x \in W \land n \in (0 \dots \|x\|)) \land (y \in I \land z \in 2_{𝑜})) \to ⟨y, 1_{𝑜} ∖ z⟩ \in (I \times 2_{𝑜})$
13	8 12	s2cld	$⊢ ((x \in W \land n \in (0 \dots \|x\|)) \land (y \in I \land z \in 2_{𝑜})) \to ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩ \in Word (I \times 2_{𝑜})$
14		splcl	$⊢ (x \in Word (I \times 2_{𝑜}) \land ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩ \in Word (I \times 2_{𝑜})) \to x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩ \in Word (I \times 2_{𝑜})$
15	6 13 14	syl2anc	$⊢ ((x \in W \land n \in (0 \dots \|x\|)) \land (y \in I \land z \in 2_{𝑜})) \to x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩ \in Word (I \times 2_{𝑜})$
16	1	efgrcl	$⊢ x \in W \to (I \in V \land W = Word (I \times 2_{𝑜}))$
17	16	simprd	$⊢ x \in W \to W = Word (I \times 2_{𝑜})$
18	17	ad2antrr	$⊢ ((x \in W \land n \in (0 \dots \|x\|)) \land (y \in I \land z \in 2_{𝑜})) \to W = Word (I \times 2_{𝑜})$
19	15 18	eleqtrrd	$⊢ ((x \in W \land n \in (0 \dots \|x\|)) \land (y \in I \land z \in 2_{𝑜})) \to x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩ \in W$
20		brxp	$⊢ x (W \times W) (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩) \leftrightarrow (x \in W \land x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩ \in W)$
21	3 19 20	sylanbrc	$⊢ ((x \in W \land n \in (0 \dots \|x\|)) \land (y \in I \land z \in 2_{𝑜})) \to x (W \times W) (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩)$
22	21	ralrimivva	$⊢ (x \in W \land n \in (0 \dots \|x\|)) \to \forall y \in I \forall z \in 2_{𝑜} x (W \times W) (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩)$
23	22	rgen2	$⊢ \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x (W \times W) (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩)$
24	1	fvexi	$⊢ W \in V$
25	24 24	xpex	$⊢ W \times W \in V$
26		ereq1	$⊢ r = W \times W \to (r Er W \leftrightarrow (W \times W) Er W)$
27		breq	$⊢ r = W \times W \to (x r (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩) \leftrightarrow x (W \times W) (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))$
28	27	2ralbidv	$⊢ r = W \times W \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 (W \times W) (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))$
29	28	2ralbidv	$⊢ r = W \times W \to (\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 \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x (W \times W) (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩))$
30	26 29	anbi12d	$⊢ r = W \times W \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⟩ ”⟩⟩)) \leftrightarrow ((W \times W) Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x (W \times W) (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩)))$
31	25 30	spcev	$⊢ ((W \times W) Er W \land \forall x \in W \forall n \in (0 \dots \|x\|) \forall y \in I \forall z \in 2_{𝑜} x (W \times W) (x splice ⟨n, n, ⟨“ ⟨y, z⟩ ⟨y, 1_{𝑜} ∖ z⟩ ”⟩⟩)) \to \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⟩ ”⟩⟩))$
32	2 23 31	mp2an	$⊢ \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⟩ ”⟩⟩))$

Metamath Proof Explorer

Theorem efglem

Proof