efgrelexlema - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > efgrelexlema		Structured version Visualization version GIF version

Theorem efgrelexlema 19716

Description: If two words 𝐴, 𝐵 are related under the free group equivalence, then there exist two extension sequences 𝑎, 𝑏 such that 𝑎 ends at 𝐴, 𝑏 ends at 𝐵, and 𝑎 and 𝐵 have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015.)

**Hypotheses**
Ref	Expression
efgval.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2_o))
efgval.r	⊢ ∼ = ( ~_FG ‘𝐼)
efgval2.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_o ↦ ⟨𝑦, (1_o ∖ 𝑧)⟩)
efgval2.t	⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2_o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
efgred.d	⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
efgred.s	⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
efgrelexlem.1	⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ∃𝑐 ∈ (^◡𝑆 “ {𝑖})∃𝑑 ∈ (^◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0)}

**Assertion**
Ref	Expression
efgrelexlema	⊢ (𝐴𝐿𝐵 ↔ ∃𝑎 ∈ (^◡𝑆 “ {𝐴})∃𝑏 ∈ (^◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0))

Distinct variable groups: 𝑎,𝑏,𝑐,𝑑,𝑖,𝑗,𝐴 𝑦,𝑎,𝑧,𝑏 𝐿,𝑎,𝑏 𝑛,𝑐,𝑡,𝑣,𝑤,𝑦,𝑧 𝑚,𝑎,𝑛,𝑡,𝑣,𝑤,𝑥,𝑀,𝑏,𝑐,𝑖,𝑗 𝑘,𝑎,𝑇,𝑏,𝑐,𝑖,𝑗,𝑚,𝑡,𝑥 𝑊,𝑎,𝑏,𝑐 𝑘,𝑑,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧,𝑊,𝑖,𝑗 ∼ ,𝑎,𝑏,𝑐,𝑑,𝑖,𝑗,𝑚,𝑡,𝑥,𝑦,𝑧 𝐵,𝑎,𝑏,𝑐,𝑑,𝑖,𝑗 𝑆,𝑎,𝑏,𝑐,𝑑,𝑖,𝑗 𝐼,𝑎,𝑏,𝑐,𝑖,𝑗,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧 𝐷,𝑎,𝑏,𝑐,𝑑,𝑖,𝑗,𝑚,𝑡 Allowed substitution hints: 𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛) 𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛) 𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛) ∼ (𝑤,𝑣,𝑘,𝑛) 𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛) 𝑇(𝑦,𝑧,𝑤,𝑣,𝑛,𝑑) 𝐼(𝑘,𝑑) 𝐿(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑖,𝑗,𝑘,𝑚,𝑛,𝑐,𝑑) 𝑀(𝑦,𝑧,𝑘,𝑑)

**Proof of Theorem efgrelexlema**
Step	Hyp	Ref	Expression
1		efgrelexlem.1	. . 3 ⊢ 𝐿 = {⟨𝑖, 𝑗⟩ ∣ ∃𝑐 ∈ (^◡𝑆 “ {𝑖})∃𝑑 ∈ (^◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0)}
2	1	bropaex12 5769	. 2 ⊢ (𝐴𝐿𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3		n0i 4333	. . . . . 6 ⊢ (𝑎 ∈ (^◡𝑆 “ {𝐴}) → ¬ (^◡𝑆 “ {𝐴}) = ∅)
4		snprc 4723	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
5		imaeq2 6060	. . . . . . . 8 ⊢ ({𝐴} = ∅ → (^◡𝑆 “ {𝐴}) = (^◡𝑆 “ ∅))
6	4, 5	sylbi 216	. . . . . . 7 ⊢ (¬ 𝐴 ∈ V → (^◡𝑆 “ {𝐴}) = (^◡𝑆 “ ∅))
7		ima0 6081	. . . . . . 7 ⊢ (^◡𝑆 “ ∅) = ∅
8	6, 7	eqtrdi 2781	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → (^◡𝑆 “ {𝐴}) = ∅)
9	3, 8	nsyl2 141	. . . . 5 ⊢ (𝑎 ∈ (^◡𝑆 “ {𝐴}) → 𝐴 ∈ V)
10		n0i 4333	. . . . . 6 ⊢ (𝑏 ∈ (^◡𝑆 “ {𝐵}) → ¬ (^◡𝑆 “ {𝐵}) = ∅)
11		snprc 4723	. . . . . . . 8 ⊢ (¬ 𝐵 ∈ V ↔ {𝐵} = ∅)
12		imaeq2 6060	. . . . . . . 8 ⊢ ({𝐵} = ∅ → (^◡𝑆 “ {𝐵}) = (^◡𝑆 “ ∅))
13	11, 12	sylbi 216	. . . . . . 7 ⊢ (¬ 𝐵 ∈ V → (^◡𝑆 “ {𝐵}) = (^◡𝑆 “ ∅))
14	13, 7	eqtrdi 2781	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → (^◡𝑆 “ {𝐵}) = ∅)
15	10, 14	nsyl2 141	. . . . 5 ⊢ (𝑏 ∈ (^◡𝑆 “ {𝐵}) → 𝐵 ∈ V)
16	9, 15	anim12i 611	. . . 4 ⊢ ((𝑎 ∈ (^◡𝑆 “ {𝐴}) ∧ 𝑏 ∈ (^◡𝑆 “ {𝐵})) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
17	16	a1d 25	. . 3 ⊢ ((𝑎 ∈ (^◡𝑆 “ {𝐴}) ∧ 𝑏 ∈ (^◡𝑆 “ {𝐵})) → ((𝑎‘0) = (𝑏‘0) → (𝐴 ∈ V ∧ 𝐵 ∈ V)))
18	17	rexlimivv 3189	. 2 ⊢ (∃𝑎 ∈ (^◡𝑆 “ {𝐴})∃𝑏 ∈ (^◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
19		fveq1 6895	. . . . . 6 ⊢ (𝑐 = 𝑎 → (𝑐‘0) = (𝑎‘0))
20	19	eqeq1d 2727	. . . . 5 ⊢ (𝑐 = 𝑎 → ((𝑐‘0) = (𝑑‘0) ↔ (𝑎‘0) = (𝑑‘0)))
21		fveq1 6895	. . . . . 6 ⊢ (𝑑 = 𝑏 → (𝑑‘0) = (𝑏‘0))
22	21	eqeq2d 2736	. . . . 5 ⊢ (𝑑 = 𝑏 → ((𝑎‘0) = (𝑑‘0) ↔ (𝑎‘0) = (𝑏‘0)))
23	20, 22	cbvrex2vw 3229	. . . 4 ⊢ (∃𝑐 ∈ (^◡𝑆 “ {𝑖})∃𝑑 ∈ (^◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0) ↔ ∃𝑎 ∈ (^◡𝑆 “ {𝑖})∃𝑏 ∈ (^◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0))
24		sneq 4640	. . . . . 6 ⊢ (𝑖 = 𝐴 → {𝑖} = {𝐴})
25	24	imaeq2d 6064	. . . . 5 ⊢ (𝑖 = 𝐴 → (^◡𝑆 “ {𝑖}) = (^◡𝑆 “ {𝐴}))
26	25	rexeqdv 3315	. . . 4 ⊢ (𝑖 = 𝐴 → (∃𝑎 ∈ (^◡𝑆 “ {𝑖})∃𝑏 ∈ (^◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑎 ∈ (^◡𝑆 “ {𝐴})∃𝑏 ∈ (^◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0)))
27	23, 26	bitrid 282	. . 3 ⊢ (𝑖 = 𝐴 → (∃𝑐 ∈ (^◡𝑆 “ {𝑖})∃𝑑 ∈ (^◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0) ↔ ∃𝑎 ∈ (^◡𝑆 “ {𝐴})∃𝑏 ∈ (^◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0)))
28		sneq 4640	. . . . . 6 ⊢ (𝑗 = 𝐵 → {𝑗} = {𝐵})
29	28	imaeq2d 6064	. . . . 5 ⊢ (𝑗 = 𝐵 → (^◡𝑆 “ {𝑗}) = (^◡𝑆 “ {𝐵}))
30	29	rexeqdv 3315	. . . 4 ⊢ (𝑗 = 𝐵 → (∃𝑏 ∈ (^◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑏 ∈ (^◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0)))
31	30	rexbidv 3168	. . 3 ⊢ (𝑗 = 𝐵 → (∃𝑎 ∈ (^◡𝑆 “ {𝐴})∃𝑏 ∈ (^◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑎 ∈ (^◡𝑆 “ {𝐴})∃𝑏 ∈ (^◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0)))
32	27, 31, 1	brabg 5541	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐿𝐵 ↔ ∃𝑎 ∈ (^◡𝑆 “ {𝐴})∃𝑏 ∈ (^◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0)))
33	2, 18, 32	pm5.21nii 377	1 ⊢ (𝐴𝐿𝐵 ↔ ∃𝑎 ∈ (^◡𝑆 “ {𝐴})∃𝑏 ∈ (^◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 394 = wceq 1533 ∈ wcel 2098 ∀wral 3050 ∃wrex 3059 {crab 3418 Vcvv 3461 ∖ cdif 3941 ∅c0 4322 {csn 4630 ⟨cop 4636 ⟨cotp 4638 ∪ ciun 4997 class class class wbr 5149 {copab 5211 ↦ cmpt 5232 I cid 5575 × cxp 5676 ^◡ccnv 5677 ran crn 5679 “ cima 5681 ‘cfv 6549 (class class class)co 7419 ∈ cmpo 7421 1_oc1o 8480 2_oc2o 8481 0cc0 11140 1c1 11141 − cmin 11476 ...cfz 13519 ..^cfzo 13662 ♯chash 14325 Word cword 14500 splice csplice 14735 ⟨“cs2 14828 ~_FG cefg 19673

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-xp 5684 df-cnv 5686 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6501 df-fv 6557

This theorem is referenced by: efgrelexlemb 19717 efgrelex 19718

W3C validator

	
		OSZAR »