Metamath Proof Explorer

Theorem efgrelexlemb

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

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

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 efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
6 efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
7 efgrelexlem.1 ⊢ 𝐿 = { ⟨ 𝑖 , 𝑗 ⟩ ∣ ∃ 𝑐 ∈ ( ◡ 𝑆 “ { 𝑖 } ) ∃ 𝑑 ∈ ( ◡ 𝑆 “ { 𝑗 } ) ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) }
8 1 2 3 4 efgval2 ⊢ ∼ = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) }
9 7 relopabiv ⊢ Rel 𝐿
10 9 a1i ⊢ ( ⊤ → Rel 𝐿 )
11 eqcom ⊢ ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ( 𝑏 ‘ 0 ) = ( 𝑎 ‘ 0 ) )
12 11 2rexbii ⊢ ( ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑏 ‘ 0 ) = ( 𝑎 ‘ 0 ) )
13 rexcom ⊢ ( ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑏 ‘ 0 ) = ( 𝑎 ‘ 0 ) ↔ ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ( 𝑏 ‘ 0 ) = ( 𝑎 ‘ 0 ) )
14 12 13 bitri ⊢ ( ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ( 𝑏 ‘ 0 ) = ( 𝑎 ‘ 0 ) )
15 1 2 3 4 5 6 7 efgrelexlema ⊢ ( 𝑓 𝐿 𝑔 ↔ ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) )
16 1 2 3 4 5 6 7 efgrelexlema ⊢ ( 𝑔 𝐿 𝑓 ↔ ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ( 𝑏 ‘ 0 ) = ( 𝑎 ‘ 0 ) )
17 14 15 16 3bitr4i ⊢ ( 𝑓 𝐿 𝑔 ↔ 𝑔 𝐿 𝑓 )
18 17 bilani ⊢ ( ( ⊤ ∧ 𝑓 𝐿 𝑔 ) → 𝑔 𝐿 𝑓 )
19 1 2 3 4 5 6 7 efgrelexlema ⊢ ( 𝑔 𝐿 ℎ ↔ ∃ 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
20 reeanv ⊢ ( ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ∧ ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) ↔ ( ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ∧ ∃ 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) )
21 1 2 3 4 5 6 efgsfo ⊢ 𝑆 : dom 𝑆 –onto→ 𝑊
22 fofn ⊢ ( 𝑆 : dom 𝑆 –onto→ 𝑊 → 𝑆 Fn dom 𝑆 )
23 21 22 ax-mp ⊢ 𝑆 Fn dom 𝑆
24 fniniseg ⊢ ( 𝑆 Fn dom 𝑆 → ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ↔ ( 𝑟 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑟 ) = 𝑔 ) ) )
25 23 24 ax-mp ⊢ ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ↔ ( 𝑟 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑟 ) = 𝑔 ) )
26 fniniseg ⊢ ( 𝑆 Fn dom 𝑆 → ( 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ↔ ( 𝑏 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑏 ) = 𝑔 ) ) )
27 23 26 ax-mp ⊢ ( 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ↔ ( 𝑏 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑏 ) = 𝑔 ) )
28 eqtr3 ⊢ ( ( ( 𝑆 ‘ 𝑟 ) = 𝑔 ∧ ( 𝑆 ‘ 𝑏 ) = 𝑔 ) → ( 𝑆 ‘ 𝑟 ) = ( 𝑆 ‘ 𝑏 ) )
29 1 2 3 4 5 6 efgred ⊢ ( ( 𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑟 ) = ( 𝑆 ‘ 𝑏 ) ) → ( 𝑟 ‘ 0 ) = ( 𝑏 ‘ 0 ) )
30 29 eqcomd ⊢ ( ( 𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑟 ) = ( 𝑆 ‘ 𝑏 ) ) → ( 𝑏 ‘ 0 ) = ( 𝑟 ‘ 0 ) )
31 30 3expa ⊢ ( ( ( 𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ) ∧ ( 𝑆 ‘ 𝑟 ) = ( 𝑆 ‘ 𝑏 ) ) → ( 𝑏 ‘ 0 ) = ( 𝑟 ‘ 0 ) )
32 28 31 sylan2 ⊢ ( ( ( 𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ) ∧ ( ( 𝑆 ‘ 𝑟 ) = 𝑔 ∧ ( 𝑆 ‘ 𝑏 ) = 𝑔 ) ) → ( 𝑏 ‘ 0 ) = ( 𝑟 ‘ 0 ) )
33 32 an4s ⊢ ( ( ( 𝑟 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑟 ) = 𝑔 ) ∧ ( 𝑏 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑏 ) = 𝑔 ) ) → ( 𝑏 ‘ 0 ) = ( 𝑟 ‘ 0 ) )
34 25 27 33 syl2anb ⊢ ( ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∧ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ) → ( 𝑏 ‘ 0 ) = ( 𝑟 ‘ 0 ) )
35 eqeq2 ⊢ ( ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) → ( ( 𝑏 ‘ 0 ) = ( 𝑟 ‘ 0 ) ↔ ( 𝑏 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) )
36 34 35 syl5ibcom ⊢ ( ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∧ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ) → ( ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) → ( 𝑏 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) )
37 36 reximdv ⊢ ( ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∧ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ) → ( ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) → ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑏 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) )
38 eqeq1 ⊢ ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) → ( ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) ↔ ( 𝑏 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) )
39 38 rexbidv ⊢ ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) → ( ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) ↔ ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑏 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) )
40 39 imbi2d ⊢ ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) → ( ( ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) → ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) ↔ ( ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) → ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑏 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) ) )
41 37 40 syl5ibrcom ⊢ ( ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∧ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ) → ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) → ( ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) → ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) ) )
42 41 rexlimdva ⊢ ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) → ( ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) → ( ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) → ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) ) )
43 42 impd ⊢ ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) → ( ( ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ∧ ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) → ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) )
44 43 rexlimiv ⊢ ( ∃ 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ∧ ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) → ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
45 44 reximi ⊢ ( ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ∧ ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) → ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
46 20 45 sylbir ⊢ ( ( ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ∧ ∃ 𝑟 ∈ ( ◡ 𝑆 “ { 𝑔 } ) ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) ) → ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
47 15 19 46 syl2anb ⊢ ( ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) → ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
48 1 2 3 4 5 6 7 efgrelexlema ⊢ ( 𝑓 𝐿 ℎ ↔ ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑠 ∈ ( ◡ 𝑆 “ { ℎ } ) ( 𝑎 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
49 47 48 sylibr ⊢ ( ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) → 𝑓 𝐿 ℎ )
50 49 adantl ⊢ ( ( ⊤ ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → 𝑓 𝐿 ℎ )
51 eqid ⊢ ( 𝑎 ‘ 0 ) = ( 𝑎 ‘ 0 )
52 fveq1 ⊢ ( 𝑏 = 𝑎 → ( 𝑏 ‘ 0 ) = ( 𝑎 ‘ 0 ) )
53 52 rspceeqv ⊢ ( ( 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∧ ( 𝑎 ‘ 0 ) = ( 𝑎 ‘ 0 ) ) → ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) )
54 51 53 mpan2 ⊢ ( 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) → ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) )
55 54 pm4.71i ⊢ ( 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ↔ ( 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∧ ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
56 fniniseg ⊢ ( 𝑆 Fn dom 𝑆 → ( 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ↔ ( 𝑎 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑎 ) = 𝑓 ) ) )
57 23 56 ax-mp ⊢ ( 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ↔ ( 𝑎 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑎 ) = 𝑓 ) )
58 55 57 bitr3i ⊢ ( ( 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∧ ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ↔ ( 𝑎 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑎 ) = 𝑓 ) )
59 58 rexbii2 ⊢ ( ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ∃ 𝑎 ∈ dom 𝑆 ( 𝑆 ‘ 𝑎 ) = 𝑓 )
60 1 2 3 4 5 6 7 efgrelexlema ⊢ ( 𝑓 𝐿 𝑓 ↔ ∃ 𝑎 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ∃ 𝑏 ∈ ( ◡ 𝑆 “ { 𝑓 } ) ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) )
61 forn ⊢ ( 𝑆 : dom 𝑆 –onto→ 𝑊 → ran 𝑆 = 𝑊 )
62 21 61 ax-mp ⊢ ran 𝑆 = 𝑊
63 62 eleq2i ⊢ ( 𝑓 ∈ ran 𝑆 ↔ 𝑓 ∈ 𝑊 )
64 fvelrnb ⊢ ( 𝑆 Fn dom 𝑆 → ( 𝑓 ∈ ran 𝑆 ↔ ∃ 𝑎 ∈ dom 𝑆 ( 𝑆 ‘ 𝑎 ) = 𝑓 ) )
65 23 64 ax-mp ⊢ ( 𝑓 ∈ ran 𝑆 ↔ ∃ 𝑎 ∈ dom 𝑆 ( 𝑆 ‘ 𝑎 ) = 𝑓 )
66 63 65 bitr3i ⊢ ( 𝑓 ∈ 𝑊 ↔ ∃ 𝑎 ∈ dom 𝑆 ( 𝑆 ‘ 𝑎 ) = 𝑓 )
67 59 60 66 3bitr4ri ⊢ ( 𝑓 ∈ 𝑊 ↔ 𝑓 𝐿 𝑓 )
68 67 a1i ⊢ ( ⊤ → ( 𝑓 ∈ 𝑊 ↔ 𝑓 𝐿 𝑓 ) )
69 10 18 50 68 iserd ⊢ ( ⊤ → 𝐿 Er 𝑊 )
70 69 mptru ⊢ 𝐿 Er 𝑊
71 simpl ⊢ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) → 𝑎 ∈ 𝑊 )
72 foelrn ⊢ ( ( 𝑆 : dom 𝑆 –onto→ 𝑊 ∧ 𝑎 ∈ 𝑊 ) → ∃ 𝑟 ∈ dom 𝑆 𝑎 = ( 𝑆 ‘ 𝑟 ) )
73 21 71 72 sylancr ⊢ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) → ∃ 𝑟 ∈ dom 𝑆 𝑎 = ( 𝑆 ‘ 𝑟 ) )
74 simprl ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → 𝑟 ∈ dom 𝑆 )
75 simprr ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → 𝑎 = ( 𝑆 ‘ 𝑟 ) )
76 75 eqcomd ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ( 𝑆 ‘ 𝑟 ) = 𝑎 )
77 fniniseg ⊢ ( 𝑆 Fn dom 𝑆 → ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑎 } ) ↔ ( 𝑟 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑟 ) = 𝑎 ) ) )
78 23 77 ax-mp ⊢ ( 𝑟 ∈ ( ◡ 𝑆 “ { 𝑎 } ) ↔ ( 𝑟 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑟 ) = 𝑎 ) )
79 74 76 78 sylanbrc ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → 𝑟 ∈ ( ◡ 𝑆 “ { 𝑎 } ) )
80 simplr ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) )
81 75 fveq2d ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑟 ) ) )
82 81 rneqd ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ran ( 𝑇 ‘ 𝑎 ) = ran ( 𝑇 ‘ ( 𝑆 ‘ 𝑟 ) ) )
83 80 82 eleqtrd ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → 𝑏 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝑟 ) ) )
84 1 2 3 4 5 6 efgsp1 ⊢ ( ( 𝑟 ∈ dom 𝑆 ∧ 𝑏 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝑟 ) ) ) → ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ∈ dom 𝑆 )
85 74 83 84 syl2anc ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ∈ dom 𝑆 )
86 1 2 3 4 5 6 efgsdm ⊢ ( 𝑟 ∈ dom 𝑆 ↔ ( 𝑟 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝑟 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑟 ) ) ( 𝑟 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑟 ‘ ( 𝑖 − 1 ) ) ) ) )
87 86 simp1bi ⊢ ( 𝑟 ∈ dom 𝑆 → 𝑟 ∈ ( Word 𝑊 ∖ { ∅ } ) )
88 87 ad2antrl ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → 𝑟 ∈ ( Word 𝑊 ∖ { ∅ } ) )
89 88 eldifad ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → 𝑟 ∈ Word 𝑊 )
90 1 2 3 4 efgtf ⊢ ( 𝑎 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑎 ) = ( 𝑓 ∈ ( 0 ... ( ♯ ‘ 𝑎 ) ) , 𝑔 ∈ ( 𝐼 × 2o ) ↦ ( 𝑎 splice ⟨ 𝑓 , 𝑓 , ⟨“ 𝑔 ( 𝑀 ‘ 𝑔 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ 𝑎 ) : ( ( 0 ... ( ♯ ‘ 𝑎 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
91 90 simprd ⊢ ( 𝑎 ∈ 𝑊 → ( 𝑇 ‘ 𝑎 ) : ( ( 0 ... ( ♯ ‘ 𝑎 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
92 91 frnd ⊢ ( 𝑎 ∈ 𝑊 → ran ( 𝑇 ‘ 𝑎 ) ⊆ 𝑊 )
93 92 sselda ⊢ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) → 𝑏 ∈ 𝑊 )
94 93 adantr ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → 𝑏 ∈ 𝑊 )
95 1 2 3 4 5 6 efgsval2 ⊢ ( ( 𝑟 ∈ Word 𝑊 ∧ 𝑏 ∈ 𝑊 ∧ ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ∈ dom 𝑆 ) → ( 𝑆 ‘ ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ) = 𝑏 )
96 89 94 85 95 syl3anc ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ( 𝑆 ‘ ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ) = 𝑏 )
97 fniniseg ⊢ ( 𝑆 Fn dom 𝑆 → ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ∈ ( ◡ 𝑆 “ { 𝑏 } ) ↔ ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ∈ dom 𝑆 ∧ ( 𝑆 ‘ ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ) = 𝑏 ) ) )
98 23 97 ax-mp ⊢ ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ∈ ( ◡ 𝑆 “ { 𝑏 } ) ↔ ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ∈ dom 𝑆 ∧ ( 𝑆 ‘ ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ) = 𝑏 ) )
99 85 96 98 sylanbrc ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ∈ ( ◡ 𝑆 “ { 𝑏 } ) )
100 94 s1cld ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ⟨“ 𝑏 ”⟩ ∈ Word 𝑊 )
101 eldifsn ⊢ ( 𝑟 ∈ ( Word 𝑊 ∖ { ∅ } ) ↔ ( 𝑟 ∈ Word 𝑊 ∧ 𝑟 ≠ ∅ ) )
102 lennncl ⊢ ( ( 𝑟 ∈ Word 𝑊 ∧ 𝑟 ≠ ∅ ) → ( ♯ ‘ 𝑟 ) ∈ ℕ )
103 101 102 sylbi ⊢ ( 𝑟 ∈ ( Word 𝑊 ∖ { ∅ } ) → ( ♯ ‘ 𝑟 ) ∈ ℕ )
104 88 103 syl ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ( ♯ ‘ 𝑟 ) ∈ ℕ )
105 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑟 ) ) ↔ ( ♯ ‘ 𝑟 ) ∈ ℕ )
106 104 105 sylibr ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑟 ) ) )
107 ccatval1 ⊢ ( ( 𝑟 ∈ Word 𝑊 ∧ ⟨“ 𝑏 ”⟩ ∈ Word 𝑊 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑟 ) ) ) → ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ‘ 0 ) = ( 𝑟 ‘ 0 ) )
108 89 100 106 107 syl3anc ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ‘ 0 ) = ( 𝑟 ‘ 0 ) )
109 108 eqcomd ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ( 𝑟 ‘ 0 ) = ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ‘ 0 ) )
110 fveq1 ⊢ ( 𝑠 = ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) → ( 𝑠 ‘ 0 ) = ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ‘ 0 ) )
111 110 rspceeqv ⊢ ( ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ∈ ( ◡ 𝑆 “ { 𝑏 } ) ∧ ( 𝑟 ‘ 0 ) = ( ( 𝑟 ++ ⟨“ 𝑏 ”⟩ ) ‘ 0 ) ) → ∃ 𝑠 ∈ ( ◡ 𝑆 “ { 𝑏 } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
112 99 109 111 syl2anc ⊢ ( ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) ∧ ( 𝑟 ∈ dom 𝑆 ∧ 𝑎 = ( 𝑆 ‘ 𝑟 ) ) ) → ∃ 𝑠 ∈ ( ◡ 𝑆 “ { 𝑏 } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
113 73 79 112 reximssdv ⊢ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) → ∃ 𝑟 ∈ ( ◡ 𝑆 “ { 𝑎 } ) ∃ 𝑠 ∈ ( ◡ 𝑆 “ { 𝑏 } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
114 1 2 3 4 5 6 7 efgrelexlema ⊢ ( 𝑎 𝐿 𝑏 ↔ ∃ 𝑟 ∈ ( ◡ 𝑆 “ { 𝑎 } ) ∃ 𝑠 ∈ ( ◡ 𝑆 “ { 𝑏 } ) ( 𝑟 ‘ 0 ) = ( 𝑠 ‘ 0 ) )
115 113 114 sylibr ⊢ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) → 𝑎 𝐿 𝑏 )
116 vex ⊢ 𝑏 ∈ V
117 vex ⊢ 𝑎 ∈ V
118 116 117 elec ⊢ ( 𝑏 ∈ [ 𝑎 ] 𝐿 ↔ 𝑎 𝐿 𝑏 )
119 115 118 sylibr ⊢ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) ) → 𝑏 ∈ [ 𝑎 ] 𝐿 )
120 119 ex ⊢ ( 𝑎 ∈ 𝑊 → ( 𝑏 ∈ ran ( 𝑇 ‘ 𝑎 ) → 𝑏 ∈ [ 𝑎 ] 𝐿 ) )
121 120 ssrdv ⊢ ( 𝑎 ∈ 𝑊 → ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝐿 )
122 121 rgen ⊢ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝐿
123 1 fvexi ⊢ 𝑊 ∈ V
124 erex ⊢ ( 𝐿 Er 𝑊 → ( 𝑊 ∈ V → 𝐿 ∈ V ) )
125 70 123 124 mp2 ⊢ 𝐿 ∈ V
126 ereq1 ⊢ ( 𝑟 = 𝐿 → ( 𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊 ) )
127 eceq2 ⊢ ( 𝑟 = 𝐿 → [ 𝑎 ] 𝑟 = [ 𝑎 ] 𝐿 )
128 127 sseq2d ⊢ ( 𝑟 = 𝐿 → ( ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ↔ ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝐿 ) )
129 128 ralbidv ⊢ ( 𝑟 = 𝐿 → ( ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ↔ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝐿 ) )
130 126 129 anbi12d ⊢ ( 𝑟 = 𝐿 → ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) ↔ ( 𝐿 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝐿 ) ) )
131 125 130 elab ⊢ ( 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) } ↔ ( 𝐿 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝐿 ) )
132 70 122 131 mpbir2an ⊢ 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) }
133 intss1 ⊢ ( 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) } → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) } ⊆ 𝐿 )
134 132 133 ax-mp ⊢ ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) ⊆ [ 𝑎 ] 𝑟 ) } ⊆ 𝐿
135 8 134 eqsstri ⊢ ∼ ⊆ 𝐿