Metamath Proof Explorer

Theorem efgval2

Description: Value of the free group construction. (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”⟩
Assertion efgval2 ⊢∼˙=⋂r|rErW∧∀x∈Wran⁡T⁡x⊆xr

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 1 2 efgval ⊢∼˙=⋂r|rErW∧∀x∈W∀m∈0…x∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
6 1 2 3 4 efgtf ⊢x∈W→T⁡x=m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩∧T⁡x:0…x×I×2𝑜⟶W
7 6 simpld ⊢x∈W→T⁡x=m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩
8 7 rneqd ⊢x∈W→ran⁡T⁡x=ran⁡m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩
9 8 sseq1d ⊢x∈W→ran⁡T⁡x⊆xr↔ran⁡m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩⊆xr
10 dfss3 ⊢ran⁡m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩⊆xr↔∀a∈ran⁡m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩a∈xr
11 ovex ⊢xsplicemm⟨“uM⁡u”⟩∈V
12 11 rgen2w ⊢∀m∈0…x∀u∈I×2𝑜xsplicemm⟨“uM⁡u”⟩∈V
13 eqid ⊢m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩=m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩
14 vex ⊢a∈V
15 vex ⊢x∈V
16 14 15 elec ⊢a∈xr↔xra
17 breq2 ⊢a=xsplicemm⟨“uM⁡u”⟩→xra↔xrxsplicemm⟨“uM⁡u”⟩
18 16 17 bitrid ⊢a=xsplicemm⟨“uM⁡u”⟩→a∈xr↔xrxsplicemm⟨“uM⁡u”⟩
19 13 18 ralrnmpo ⊢∀m∈0…x∀u∈I×2𝑜xsplicemm⟨“uM⁡u”⟩∈V→∀a∈ran⁡m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩a∈xr↔∀m∈0…x∀u∈I×2𝑜xrxsplicemm⟨“uM⁡u”⟩
20 12 19 ax-mp ⊢∀a∈ran⁡m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩a∈xr↔∀m∈0…x∀u∈I×2𝑜xrxsplicemm⟨“uM⁡u”⟩
21 id ⊢u=ab→u=ab
22 fveq2 ⊢u=ab→M⁡u=M⁡ab
23 df-ov ⊢aMb=M⁡ab
24 22 23 eqtr4di ⊢u=ab→M⁡u=aMb
25 21 24 s2eqd ⊢u=ab→⟨“uM⁡u”⟩=⟨“abaMb”⟩
26 25 oteq3d ⊢u=ab→mm⟨“uM⁡u”⟩=mm⟨“abaMb”⟩
27 26 oveq2d ⊢u=ab→xsplicemm⟨“uM⁡u”⟩=xsplicemm⟨“abaMb”⟩
28 27 breq2d ⊢u=ab→xrxsplicemm⟨“uM⁡u”⟩↔xrxsplicemm⟨“abaMb”⟩
29 28 ralxp ⊢∀u∈I×2𝑜xrxsplicemm⟨“uM⁡u”⟩↔∀a∈I∀b∈2𝑜xrxsplicemm⟨“abaMb”⟩
30 eqidd ⊢a∈I∧b∈2𝑜→ab=ab
31 3 efgmval ⊢a∈I∧b∈2𝑜→aMb=a1𝑜∖b
32 30 31 s2eqd ⊢a∈I∧b∈2𝑜→⟨“abaMb”⟩=⟨“aba1𝑜∖b”⟩
33 32 oteq3d ⊢a∈I∧b∈2𝑜→mm⟨“abaMb”⟩=mm⟨“aba1𝑜∖b”⟩
34 33 oveq2d ⊢a∈I∧b∈2𝑜→xsplicemm⟨“abaMb”⟩=xsplicemm⟨“aba1𝑜∖b”⟩
35 34 breq2d ⊢a∈I∧b∈2𝑜→xrxsplicemm⟨“abaMb”⟩↔xrxsplicemm⟨“aba1𝑜∖b”⟩
36 35 ralbidva ⊢a∈I→∀b∈2𝑜xrxsplicemm⟨“abaMb”⟩↔∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
37 36 ralbiia ⊢∀a∈I∀b∈2𝑜xrxsplicemm⟨“abaMb”⟩↔∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
38 29 37 bitri ⊢∀u∈I×2𝑜xrxsplicemm⟨“uM⁡u”⟩↔∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
39 38 ralbii ⊢∀m∈0…x∀u∈I×2𝑜xrxsplicemm⟨“uM⁡u”⟩↔∀m∈0…x∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
40 20 39 bitri ⊢∀a∈ran⁡m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩a∈xr↔∀m∈0…x∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
41 10 40 bitri ⊢ran⁡m∈0…x,u∈I×2𝑜⟼xsplicemm⟨“uM⁡u”⟩⊆xr↔∀m∈0…x∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
42 9 41 bitrdi ⊢x∈W→ran⁡T⁡x⊆xr↔∀m∈0…x∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
43 42 ralbiia ⊢∀x∈Wran⁡T⁡x⊆xr↔∀x∈W∀m∈0…x∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
44 43 anbi2i ⊢rErW∧∀x∈Wran⁡T⁡x⊆xr↔rErW∧∀x∈W∀m∈0…x∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
45 44 abbii ⊢r|rErW∧∀x∈Wran⁡T⁡x⊆xr=r|rErW∧∀x∈W∀m∈0…x∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
46 45 inteqi ⊢⋂r|rErW∧∀x∈Wran⁡T⁡x⊆xr=⋂r|rErW∧∀x∈W∀m∈0…x∀a∈I∀b∈2𝑜xrxsplicemm⟨“aba1𝑜∖b”⟩
47 5 46 eqtr4i ⊢∼˙=⋂r|rErW∧∀x∈Wran⁡T⁡x⊆xr