Metamath Proof Explorer

Theorem efgi2

Description: Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-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 efgi2 ⊢A∈W∧B∈ran⁡T⁡A→A∼˙B

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 fveq2 ⊢a=A→T⁡a=T⁡A
6 5 rneqd ⊢a=A→ran⁡T⁡a=ran⁡T⁡A
7 eceq1 ⊢a=A→ar=Ar
8 6 7 sseq12d ⊢a=A→ran⁡T⁡a⊆ar↔ran⁡T⁡A⊆Ar
9 8 rspcv ⊢A∈W→∀a∈Wran⁡T⁡a⊆ar→ran⁡T⁡A⊆Ar
10 9 adantr ⊢A∈W∧B∈ran⁡T⁡A→∀a∈Wran⁡T⁡a⊆ar→ran⁡T⁡A⊆Ar
11 ssel ⊢ran⁡T⁡A⊆Ar→B∈ran⁡T⁡A→B∈Ar
12 11 com12 ⊢B∈ran⁡T⁡A→ran⁡T⁡A⊆Ar→B∈Ar
13 simpl ⊢B∈Ar∧A∈W→B∈Ar
14 elecg ⊢B∈Ar∧A∈W→B∈Ar↔ArB
15 13 14 mpbid ⊢B∈Ar∧A∈W→ArB
16 df-br ⊢ArB↔AB∈r
17 15 16 sylib ⊢B∈Ar∧A∈W→AB∈r
18 17 expcom ⊢A∈W→B∈Ar→AB∈r
19 12 18 sylan9r ⊢A∈W∧B∈ran⁡T⁡A→ran⁡T⁡A⊆Ar→AB∈r
20 10 19 syld ⊢A∈W∧B∈ran⁡T⁡A→∀a∈Wran⁡T⁡a⊆ar→AB∈r
21 20 adantld ⊢A∈W∧B∈ran⁡T⁡A→rErW∧∀a∈Wran⁡T⁡a⊆ar→AB∈r
22 21 alrimiv ⊢A∈W∧B∈ran⁡T⁡A→∀rrErW∧∀a∈Wran⁡T⁡a⊆ar→AB∈r
23 opex ⊢AB∈V
24 23 elintab ⊢AB∈⋂r|rErW∧∀a∈Wran⁡T⁡a⊆ar↔∀rrErW∧∀a∈Wran⁡T⁡a⊆ar→AB∈r
25 22 24 sylibr ⊢A∈W∧B∈ran⁡T⁡A→AB∈⋂r|rErW∧∀a∈Wran⁡T⁡a⊆ar
26 1 2 3 4 efgval2 ⊢∼˙=⋂r|rErW∧∀a∈Wran⁡T⁡a⊆ar
27 25 26 eleqtrrdi ⊢A∈W∧B∈ran⁡T⁡A→AB∈∼˙
28 df-br ⊢A∼˙B↔AB∈∼˙
29 27 28 sylibr ⊢A∈W∧B∈ran⁡T⁡A→A∼˙B