efgi

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	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
	efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
Assertion	efgi	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2_o ) ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
2		efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
3		fveq2	⊢ ( 𝑢 = 𝐴 → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ 𝐴 ) )
4	3	oveq2d	⊢ ( 𝑢 = 𝐴 → ( 0 ... ( ♯ ‘ 𝑢 ) ) = ( 0 ... ( ♯ ‘ 𝐴 ) ) )
5		id	⊢ ( 𝑢 = 𝐴 → 𝑢 = 𝐴 )
6		oveq1	⊢ ( 𝑢 = 𝐴 → ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) = ( 𝐴 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) )
7	5 6	breq12d	⊢ ( 𝑢 = 𝐴 → ( 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
8	7	2ralbidv	⊢ ( 𝑢 = 𝐴 → ( ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
9	4 8	raleqbidv	⊢ ( 𝑢 = 𝐴 → ( ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
10	9	rspcv	⊢ ( 𝐴 ∈ 𝑊 → ( ∀ 𝑢 ∈ 𝑊 ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
11		oteq1	⊢ ( 𝑖 = 𝑁 → ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ )
12		oteq2	⊢ ( 𝑖 = 𝑁 → ⟨ 𝑁 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ )
13	11 12	eqtrd	⊢ ( 𝑖 = 𝑁 → ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ )
14	13	oveq2d	⊢ ( 𝑖 = 𝑁 → ( 𝐴 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) = ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) )
15	14	breq2d	⊢ ( 𝑖 = 𝑁 → ( 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
16	15	2ralbidv	⊢ ( 𝑖 = 𝑁 → ( ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
17	16	rspcv	⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) → ( ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
18	10 17	sylan9	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ∀ 𝑢 ∈ 𝑊 ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
19		opeq1	⊢ ( 𝑎 = 𝐽 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐽 , 𝑏 ⟩ )
20		opeq1	⊢ ( 𝑎 = 𝐽 → ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ = ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ )
21	19 20	s2eqd	⊢ ( 𝑎 = 𝐽 → ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ = ⟨“ ⟨ 𝐽 , 𝑏 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ )
22	21	oteq3d	⊢ ( 𝑎 = 𝐽 → ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝑏 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ )
23	22	oveq2d	⊢ ( 𝑎 = 𝐽 → ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) = ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝑏 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) )
24	23	breq2d	⊢ ( 𝑎 = 𝐽 → ( 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝑏 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) )
25		opeq2	⊢ ( 𝑏 = 𝐾 → ⟨ 𝐽 , 𝑏 ⟩ = ⟨ 𝐽 , 𝐾 ⟩ )
26		difeq2	⊢ ( 𝑏 = 𝐾 → ( 1_o ∖ 𝑏 ) = ( 1_o ∖ 𝐾 ) )
27	26	opeq2d	⊢ ( 𝑏 = 𝐾 → ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ = ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ )
28	25 27	s2eqd	⊢ ( 𝑏 = 𝐾 → ⟨“ ⟨ 𝐽 , 𝑏 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ = ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ )
29	28	oteq3d	⊢ ( 𝑏 = 𝐾 → ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝑏 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ )
30	29	oveq2d	⊢ ( 𝑏 = 𝐾 → ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝑏 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) = ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) )
31	30	breq2d	⊢ ( 𝑏 = 𝐾 → ( 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝑏 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ) )
32		df-br	⊢ ( 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ↔ ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ 𝑟 )
33	31 32	bitrdi	⊢ ( 𝑏 = 𝐾 → ( 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝑏 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ↔ ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ 𝑟 ) )
34	24 33	rspc2v	⊢ ( ( 𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2_o ) → ( ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝐴 𝑟 ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ 𝑟 ) )
35	18 34	sylan9	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2_o ) ) → ( ∀ 𝑢 ∈ 𝑊 ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) → ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ 𝑟 ) )
36	35	adantld	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2_o ) ) → ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑢 ∈ 𝑊 ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ 𝑟 ) )
37	36	alrimiv	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2_o ) ) → ∀ 𝑟 ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑢 ∈ 𝑊 ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ 𝑟 ) )
38		opex	⊢ ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ V
39	38	elintab	⊢ ( ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑢 ∈ 𝑊 ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } ↔ ∀ 𝑟 ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑢 ∈ 𝑊 ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) → ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ 𝑟 ) )
40	37 39	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2_o ) ) → ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑢 ∈ 𝑊 ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) } )
41	1 2	efgval	⊢ ∼ = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑢 ∈ 𝑊 ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 2_o 𝑢 𝑟 ( 𝑢 splice ⟨ 𝑖 , 𝑖 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1_o ∖ 𝑏 ) ⟩ ”⟩ ⟩ ) ) }
42	40 41	eleqtrrdi	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2_o ) ) → ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ ∼ )
43		df-br	⊢ ( 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ↔ ⟨ 𝐴 , ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) ⟩ ∈ ∼ )
44	42 43	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2_o ) ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 𝐾 ⟩ ⟨ 𝐽 , ( 1_o ∖ 𝐾 ) ⟩ ”⟩ ⟩ ) )

Metamath Proof Explorer

Theorem efgi

Proof