Metamath Proof Explorer

Theorem efgsval

Description: Value of the auxiliary function S defining a sequence of extensions. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses efgval.w ⊢W=I⁡WordI×2𝑜
efgval.r ⊢∼˙=~FG⁡I
efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
Assertion efgsval ⊢F∈dom⁡S→S⁡F=F⁡F−1

Proof

Step Hyp Ref Expression
1 efgval.w ⊢W=I⁡WordI×2𝑜
2 efgval.r ⊢∼˙=~FG⁡I
3 efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
4 efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
5 efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
6 efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
7 id ⊢f=F→f=F
8 fveq2 ⊢f=F→f=F
9 8 oveq1d ⊢f=F→f−1=F−1
10 7 9 fveq12d ⊢f=F→f⁡f−1=F⁡F−1
11 id ⊢m=f→m=f
12 fveq2 ⊢m=f→m=f
13 12 oveq1d ⊢m=f→m−1=f−1
14 11 13 fveq12d ⊢m=f→m⁡m−1=f⁡f−1
15 14 cbvmptv ⊢m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1=f∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼f⁡f−1
16 6 15 eqtri ⊢S=f∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼f⁡f−1
17 fvex ⊢F⁡F−1∈V
18 10 16 17 fvmpt ⊢F∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1→S⁡F=F⁡F−1
19 1 2 3 4 5 6 efgsf ⊢S:t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟶W
20 19 fdmi ⊢dom⁡S=t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1
21 18 20 eleq2s ⊢F∈dom⁡S→S⁡F=F⁡F−1