Metamath Proof Explorer


Theorem efgval2

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

Ref Expression
Hypotheses efgval.w 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r = ( ~FG𝐼 )
efgval2.m 𝑀 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ )
efgval2.t 𝑇 = ( 𝑣𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀𝑤 ) ”⟩ ⟩ ) ) )
Assertion efgval2 = { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥𝑊 ran ( 𝑇𝑥 ) ⊆ [ 𝑥 ] 𝑟 ) }

Proof

Step Hyp Ref Expression
1 efgval.w 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r = ( ~FG𝐼 )
3 efgval2.m 𝑀 = ( 𝑦𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o𝑧 ) ⟩ )
4 efgval2.t 𝑇 = ( 𝑣𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀𝑤 ) ”⟩ ⟩ ) ) )
5 1 2 efgval = { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥𝑊𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) ) }
6 1 2 3 4 efgtf ( 𝑥𝑊 → ( ( 𝑇𝑥 ) = ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) ∧ ( 𝑇𝑥 ) : ( ( 0 ... ( ♯ ‘ 𝑥 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
7 6 simpld ( 𝑥𝑊 → ( 𝑇𝑥 ) = ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) )
8 7 rneqd ( 𝑥𝑊 → ran ( 𝑇𝑥 ) = ran ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) )
9 8 sseq1d ( 𝑥𝑊 → ( ran ( 𝑇𝑥 ) ⊆ [ 𝑥 ] 𝑟 ↔ ran ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) ⊆ [ 𝑥 ] 𝑟 ) )
10 dfss3 ( ran ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) ⊆ [ 𝑥 ] 𝑟 ↔ ∀ 𝑎 ∈ ran ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) 𝑎 ∈ [ 𝑥 ] 𝑟 )
11 ovex ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ∈ V
12 11 rgen2w 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( 𝐼 × 2o ) ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ∈ V
13 eqid ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) = ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) )
14 vex 𝑎 ∈ V
15 vex 𝑥 ∈ V
16 14 15 elec ( 𝑎 ∈ [ 𝑥 ] 𝑟𝑥 𝑟 𝑎 )
17 breq2 ( 𝑎 = ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) → ( 𝑥 𝑟 𝑎𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) )
18 16 17 syl5bb ( 𝑎 = ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) → ( 𝑎 ∈ [ 𝑥 ] 𝑟𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) )
19 13 18 ralrnmpo ( ∀ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( 𝐼 × 2o ) ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ∈ V → ( ∀ 𝑎 ∈ ran ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) 𝑎 ∈ [ 𝑥 ] 𝑟 ↔ ∀ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( 𝐼 × 2o ) 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) )
20 12 19 ax-mp ( ∀ 𝑎 ∈ ran ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) 𝑎 ∈ [ 𝑥 ] 𝑟 ↔ ∀ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( 𝐼 × 2o ) 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) )
21 id ( 𝑢 = ⟨ 𝑎 , 𝑏 ⟩ → 𝑢 = ⟨ 𝑎 , 𝑏 ⟩ )
22 fveq2 ( 𝑢 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀𝑢 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) )
23 df-ov ( 𝑎 𝑀 𝑏 ) = ( 𝑀 ‘ ⟨ 𝑎 , 𝑏 ⟩ )
24 22 23 eqtr4di ( 𝑢 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑀𝑢 ) = ( 𝑎 𝑀 𝑏 ) )
25 21 24 s2eqd ( 𝑢 = ⟨ 𝑎 , 𝑏 ⟩ → ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ = ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ )
26 25 oteq3d ( 𝑢 = ⟨ 𝑎 , 𝑏 ⟩ → ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ = ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ ⟩ )
27 26 oveq2d ( 𝑢 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) = ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ ⟩ ) )
28 27 breq2d ( 𝑢 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ↔ 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ ⟩ ) ) )
29 28 ralxp ( ∀ 𝑢 ∈ ( 𝐼 × 2o ) 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ↔ ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ ⟩ ) )
30 eqidd ( ( 𝑎𝐼𝑏 ∈ 2o ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
31 3 efgmval ( ( 𝑎𝐼𝑏 ∈ 2o ) → ( 𝑎 𝑀 𝑏 ) = ⟨ 𝑎 , ( 1o𝑏 ) ⟩ )
32 30 31 s2eqd ( ( 𝑎𝐼𝑏 ∈ 2o ) → ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ = ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ )
33 32 oteq3d ( ( 𝑎𝐼𝑏 ∈ 2o ) → ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ ⟩ = ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ )
34 33 oveq2d ( ( 𝑎𝐼𝑏 ∈ 2o ) → ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ ⟩ ) = ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) )
35 34 breq2d ( ( 𝑎𝐼𝑏 ∈ 2o ) → ( 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ ⟩ ) ↔ 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) ) )
36 35 ralbidva ( 𝑎𝐼 → ( ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ ⟩ ) ↔ ∀ 𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) ) )
37 36 ralbiia ( ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ( 𝑎 𝑀 𝑏 ) ”⟩ ⟩ ) ↔ ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) )
38 29 37 bitri ( ∀ 𝑢 ∈ ( 𝐼 × 2o ) 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ↔ ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) )
39 38 ralbii ( ∀ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( 𝐼 × 2o ) 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ↔ ∀ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) )
40 20 39 bitri ( ∀ 𝑎 ∈ ran ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) 𝑎 ∈ [ 𝑥 ] 𝑟 ↔ ∀ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) )
41 10 40 bitri ( ran ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) , 𝑢 ∈ ( 𝐼 × 2o ) ↦ ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ 𝑢 ( 𝑀𝑢 ) ”⟩ ⟩ ) ) ⊆ [ 𝑥 ] 𝑟 ↔ ∀ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) )
42 9 41 bitrdi ( 𝑥𝑊 → ( ran ( 𝑇𝑥 ) ⊆ [ 𝑥 ] 𝑟 ↔ ∀ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) ) )
43 42 ralbiia ( ∀ 𝑥𝑊 ran ( 𝑇𝑥 ) ⊆ [ 𝑥 ] 𝑟 ↔ ∀ 𝑥𝑊𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) )
44 43 anbi2i ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑥𝑊 ran ( 𝑇𝑥 ) ⊆ [ 𝑥 ] 𝑟 ) ↔ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥𝑊𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) ) )
45 44 abbii { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥𝑊 ran ( 𝑇𝑥 ) ⊆ [ 𝑥 ] 𝑟 ) } = { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥𝑊𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) ) }
46 45 inteqi { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥𝑊 ran ( 𝑇𝑥 ) ⊆ [ 𝑥 ] 𝑟 ) } = { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥𝑊𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∀ 𝑎𝐼𝑏 ∈ 2o 𝑥 𝑟 ( 𝑥 splice ⟨ 𝑚 , 𝑚 , ⟨“ ⟨ 𝑎 , 𝑏 ⟩ ⟨ 𝑎 , ( 1o𝑏 ) ⟩ ”⟩ ⟩ ) ) }
47 5 46 eqtr4i = { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑥𝑊 ran ( 𝑇𝑥 ) ⊆ [ 𝑥 ] 𝑟 ) }