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