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 bitrid ⊢ ( 𝑎 = ( 𝑥 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 ( 𝑇 ‘ 𝑥 ) ⊆ [ 𝑥 ] 𝑟 ) }