Metamath Proof Explorer

Theorem efgsfo

Description: For any word, there is a sequence of extensions starting at a reduced word and ending at the target word, such that each word in the chain is an extension of the previous (inserting an element and its inverse at adjacent indices somewhere in the sequence). (Contributed by Mario Carneiro, 27-Sep-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 ) ) )
Assertion efgsfo 𝑆 : dom 𝑆 –onto→ 𝑊

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 1 2 3 4 5 6 efgsf ⊢ 𝑆 : { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ⟶ 𝑊
8 7 fdmi ⊢ dom 𝑆 = { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) }
9 8 feq2i ⊢ ( 𝑆 : dom 𝑆 ⟶ 𝑊 ↔ 𝑆 : { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ⟶ 𝑊 )
10 7 9 mpbir ⊢ 𝑆 : dom 𝑆 ⟶ 𝑊
11 frn ⊢ ( 𝑆 : dom 𝑆 ⟶ 𝑊 → ran 𝑆 ⊆ 𝑊 )
12 10 11 ax-mp ⊢ ran 𝑆 ⊆ 𝑊
13 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
14 1 13 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
15 14 sseli ⊢ ( 𝑐 ∈ 𝑊 → 𝑐 ∈ Word ( 𝐼 × 2o ) )
16 lencl ⊢ ( 𝑐 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝑐 ) ∈ ℕ0 )
17 15 16 syl ⊢ ( 𝑐 ∈ 𝑊 → ( ♯ ‘ 𝑐 ) ∈ ℕ0 )
18 peano2nn0 ⊢ ( ( ♯ ‘ 𝑐 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑐 ) + 1 ) ∈ ℕ0 )
19 14 sseli ⊢ ( 𝑎 ∈ 𝑊 → 𝑎 ∈ Word ( 𝐼 × 2o ) )
20 lencl ⊢ ( 𝑎 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝑎 ) ∈ ℕ0 )
21 19 20 syl ⊢ ( 𝑎 ∈ 𝑊 → ( ♯ ‘ 𝑎 ) ∈ ℕ0 )
22 nn0nlt0 ⊢ ( ( ♯ ‘ 𝑎 ) ∈ ℕ0 → ¬ ( ♯ ‘ 𝑎 ) < 0 )
23 breq2 ⊢ ( 𝑏 = 0 → ( ( ♯ ‘ 𝑎 ) < 𝑏 ↔ ( ♯ ‘ 𝑎 ) < 0 ) )
24 23 notbid ⊢ ( 𝑏 = 0 → ( ¬ ( ♯ ‘ 𝑎 ) < 𝑏 ↔ ¬ ( ♯ ‘ 𝑎 ) < 0 ) )
25 22 24 syl5ibr ⊢ ( 𝑏 = 0 → ( ( ♯ ‘ 𝑎 ) ∈ ℕ0 → ¬ ( ♯ ‘ 𝑎 ) < 𝑏 ) )
26 21 25 syl5 ⊢ ( 𝑏 = 0 → ( 𝑎 ∈ 𝑊 → ¬ ( ♯ ‘ 𝑎 ) < 𝑏 ) )
27 26 ralrimiv ⊢ ( 𝑏 = 0 → ∀ 𝑎 ∈ 𝑊 ¬ ( ♯ ‘ 𝑎 ) < 𝑏 )
28 rabeq0 ⊢ ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑏 } = ∅ ↔ ∀ 𝑎 ∈ 𝑊 ¬ ( ♯ ‘ 𝑎 ) < 𝑏 )
29 27 28 sylibr ⊢ ( 𝑏 = 0 → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑏 } = ∅ )
30 29 sseq1d ⊢ ( 𝑏 = 0 → ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑏 } ⊆ ran 𝑆 ↔ ∅ ⊆ ran 𝑆 ) )
31 breq2 ⊢ ( 𝑏 = 𝑑 → ( ( ♯ ‘ 𝑎 ) < 𝑏 ↔ ( ♯ ‘ 𝑎 ) < 𝑑 ) )
32 31 rabbidv ⊢ ( 𝑏 = 𝑑 → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑏 } = { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } )
33 32 sseq1d ⊢ ( 𝑏 = 𝑑 → ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑏 } ⊆ ran 𝑆 ↔ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) )
34 breq2 ⊢ ( 𝑏 = ( 𝑑 + 1 ) → ( ( ♯ ‘ 𝑎 ) < 𝑏 ↔ ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) ) )
35 34 rabbidv ⊢ ( 𝑏 = ( 𝑑 + 1 ) → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑏 } = { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) } )
36 35 sseq1d ⊢ ( 𝑏 = ( 𝑑 + 1 ) → ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑏 } ⊆ ran 𝑆 ↔ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) } ⊆ ran 𝑆 ) )
37 breq2 ⊢ ( 𝑏 = ( ( ♯ ‘ 𝑐 ) + 1 ) → ( ( ♯ ‘ 𝑎 ) < 𝑏 ↔ ( ♯ ‘ 𝑎 ) < ( ( ♯ ‘ 𝑐 ) + 1 ) ) )
38 37 rabbidv ⊢ ( 𝑏 = ( ( ♯ ‘ 𝑐 ) + 1 ) → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑏 } = { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( ( ♯ ‘ 𝑐 ) + 1 ) } )
39 38 sseq1d ⊢ ( 𝑏 = ( ( ♯ ‘ 𝑐 ) + 1 ) → ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑏 } ⊆ ran 𝑆 ↔ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( ( ♯ ‘ 𝑐 ) + 1 ) } ⊆ ran 𝑆 ) )
40 0ss ⊢ ∅ ⊆ ran 𝑆
41 simpr ⊢ ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 )
42 fveqeq2 ⊢ ( 𝑎 = 𝑐 → ( ( ♯ ‘ 𝑎 ) = 𝑑 ↔ ( ♯ ‘ 𝑐 ) = 𝑑 ) )
43 42 cbvrabv ⊢ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) = 𝑑 } = { 𝑐 ∈ 𝑊 ∣ ( ♯ ‘ 𝑐 ) = 𝑑 }
44 eliun ⊢ ( 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑊 𝑐 ∈ ran ( 𝑇 ‘ 𝑥 ) )
45 fveq2 ⊢ ( 𝑥 = 𝑏 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑏 ) )
46 45 rneqd ⊢ ( 𝑥 = 𝑏 → ran ( 𝑇 ‘ 𝑥 ) = ran ( 𝑇 ‘ 𝑏 ) )
47 46 eleq2d ⊢ ( 𝑥 = 𝑏 → ( 𝑐 ∈ ran ( 𝑇 ‘ 𝑥 ) ↔ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) )
48 47 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝑊 𝑐 ∈ ran ( 𝑇 ‘ 𝑥 ) ↔ ∃ 𝑏 ∈ 𝑊 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) )
49 44 48 bitri ⊢ ( 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ↔ ∃ 𝑏 ∈ 𝑊 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) )
50 simpl1r ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 )
51 fveq2 ⊢ ( 𝑎 = 𝑏 → ( ♯ ‘ 𝑎 ) = ( ♯ ‘ 𝑏 ) )
52 51 breq1d ⊢ ( 𝑎 = 𝑏 → ( ( ♯ ‘ 𝑎 ) < 𝑑 ↔ ( ♯ ‘ 𝑏 ) < 𝑑 ) )
53 simprl ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → 𝑏 ∈ 𝑊 )
54 14 53 sseldi ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → 𝑏 ∈ Word ( 𝐼 × 2o ) )
55 lencl ⊢ ( 𝑏 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝑏 ) ∈ ℕ0 )
56 54 55 syl ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → ( ♯ ‘ 𝑏 ) ∈ ℕ0 )
57 56 nn0red ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → ( ♯ ‘ 𝑏 ) ∈ ℝ )
58 2rp ⊢ 2 ∈ ℝ+
59 ltaddrp ⊢ ( ( ( ♯ ‘ 𝑏 ) ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ♯ ‘ 𝑏 ) < ( ( ♯ ‘ 𝑏 ) + 2 ) )
60 57 58 59 sylancl ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → ( ♯ ‘ 𝑏 ) < ( ( ♯ ‘ 𝑏 ) + 2 ) )
61 1 2 3 4 efgtlen ⊢ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) → ( ♯ ‘ 𝑐 ) = ( ( ♯ ‘ 𝑏 ) + 2 ) )
62 61 adantl ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → ( ♯ ‘ 𝑐 ) = ( ( ♯ ‘ 𝑏 ) + 2 ) )
63 simpl3 ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → ( ♯ ‘ 𝑐 ) = 𝑑 )
64 62 63 eqtr3d ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → ( ( ♯ ‘ 𝑏 ) + 2 ) = 𝑑 )
65 60 64 breqtrd ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → ( ♯ ‘ 𝑏 ) < 𝑑 )
66 52 53 65 elrabd ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → 𝑏 ∈ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } )
67 50 66 sseldd ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → 𝑏 ∈ ran 𝑆 )
68 ffn ⊢ ( 𝑆 : dom 𝑆 ⟶ 𝑊 → 𝑆 Fn dom 𝑆 )
69 10 68 ax-mp ⊢ 𝑆 Fn dom 𝑆
70 fvelrnb ⊢ ( 𝑆 Fn dom 𝑆 → ( 𝑏 ∈ ran 𝑆 ↔ ∃ 𝑜 ∈ dom 𝑆 ( 𝑆 ‘ 𝑜 ) = 𝑏 ) )
71 69 70 ax-mp ⊢ ( 𝑏 ∈ ran 𝑆 ↔ ∃ 𝑜 ∈ dom 𝑆 ( 𝑆 ‘ 𝑜 ) = 𝑏 )
72 67 71 sylib ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → ∃ 𝑜 ∈ dom 𝑆 ( 𝑆 ‘ 𝑜 ) = 𝑏 )
73 simprrl ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → 𝑜 ∈ dom 𝑆 )
74 1 2 3 4 5 6 efgsdm ⊢ ( 𝑜 ∈ dom 𝑆 ↔ ( 𝑜 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝑜 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝑜 ) ) ( 𝑜 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝑜 ‘ ( 𝑖 − 1 ) ) ) ) )
75 74 simp1bi ⊢ ( 𝑜 ∈ dom 𝑆 → 𝑜 ∈ ( Word 𝑊 ∖ { ∅ } ) )
76 eldifi ⊢ ( 𝑜 ∈ ( Word 𝑊 ∖ { ∅ } ) → 𝑜 ∈ Word 𝑊 )
77 73 75 76 3syl ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → 𝑜 ∈ Word 𝑊 )
78 simpl2 ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → 𝑐 ∈ 𝑊 )
79 simprlr ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) )
80 simprrr ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → ( 𝑆 ‘ 𝑜 ) = 𝑏 )
81 80 fveq2d ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → ( 𝑇 ‘ ( 𝑆 ‘ 𝑜 ) ) = ( 𝑇 ‘ 𝑏 ) )
82 81 rneqd ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → ran ( 𝑇 ‘ ( 𝑆 ‘ 𝑜 ) ) = ran ( 𝑇 ‘ 𝑏 ) )
83 79 82 eleqtrrd ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → 𝑐 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝑜 ) ) )
84 1 2 3 4 5 6 efgsp1 ⊢ ( ( 𝑜 ∈ dom 𝑆 ∧ 𝑐 ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝑜 ) ) ) → ( 𝑜 ++ ⟨“ 𝑐 ”⟩ ) ∈ dom 𝑆 )
85 73 83 84 syl2anc ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → ( 𝑜 ++ ⟨“ 𝑐 ”⟩ ) ∈ dom 𝑆 )
86 1 2 3 4 5 6 efgsval2 ⊢ ( ( 𝑜 ∈ Word 𝑊 ∧ 𝑐 ∈ 𝑊 ∧ ( 𝑜 ++ ⟨“ 𝑐 ”⟩ ) ∈ dom 𝑆 ) → ( 𝑆 ‘ ( 𝑜 ++ ⟨“ 𝑐 ”⟩ ) ) = 𝑐 )
87 77 78 85 86 syl3anc ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → ( 𝑆 ‘ ( 𝑜 ++ ⟨“ 𝑐 ”⟩ ) ) = 𝑐 )
88 fnfvelrn ⊢ ( ( 𝑆 Fn dom 𝑆 ∧ ( 𝑜 ++ ⟨“ 𝑐 ”⟩ ) ∈ dom 𝑆 ) → ( 𝑆 ‘ ( 𝑜 ++ ⟨“ 𝑐 ”⟩ ) ) ∈ ran 𝑆 )
89 69 85 88 sylancr ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → ( 𝑆 ‘ ( 𝑜 ++ ⟨“ 𝑐 ”⟩ ) ) ∈ ran 𝑆 )
90 87 89 eqeltrrd ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) ) → 𝑐 ∈ ran 𝑆 )
91 90 anassrs ⊢ ( ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) ∧ ( 𝑜 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝑜 ) = 𝑏 ) ) → 𝑐 ∈ ran 𝑆 )
92 72 91 rexlimddv ⊢ ( ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) ∧ ( 𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) ) ) → 𝑐 ∈ ran 𝑆 )
93 92 rexlimdvaa ⊢ ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) → ( ∃ 𝑏 ∈ 𝑊 𝑐 ∈ ran ( 𝑇 ‘ 𝑏 ) → 𝑐 ∈ ran 𝑆 ) )
94 49 93 syl5bi ⊢ ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) → ( 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) → 𝑐 ∈ ran 𝑆 ) )
95 eldif ⊢ ( 𝑐 ∈ ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) ↔ ( 𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) )
96 5 eleq2i ⊢ ( 𝑐 ∈ 𝐷 ↔ 𝑐 ∈ ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) )
97 1 2 3 4 5 6 efgs1 ⊢ ( 𝑐 ∈ 𝐷 → ⟨“ 𝑐 ”⟩ ∈ dom 𝑆 )
98 96 97 sylbir ⊢ ( 𝑐 ∈ ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → ⟨“ 𝑐 ”⟩ ∈ dom 𝑆 )
99 95 98 sylbir ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → ⟨“ 𝑐 ”⟩ ∈ dom 𝑆 )
100 1 2 3 4 5 6 efgsval ⊢ ( ⟨“ 𝑐 ”⟩ ∈ dom 𝑆 → ( 𝑆 ‘ ⟨“ 𝑐 ”⟩ ) = ( ⟨“ 𝑐 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝑐 ”⟩ ) − 1 ) ) )
101 99 100 syl ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → ( 𝑆 ‘ ⟨“ 𝑐 ”⟩ ) = ( ⟨“ 𝑐 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝑐 ”⟩ ) − 1 ) ) )
102 s1len ⊢ ( ♯ ‘ ⟨“ 𝑐 ”⟩ ) = 1
103 102 oveq1i ⊢ ( ( ♯ ‘ ⟨“ 𝑐 ”⟩ ) − 1 ) = ( 1 − 1 )
104 1m1e0 ⊢ ( 1 − 1 ) = 0
105 103 104 eqtri ⊢ ( ( ♯ ‘ ⟨“ 𝑐 ”⟩ ) − 1 ) = 0
106 105 fveq2i ⊢ ( ⟨“ 𝑐 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝑐 ”⟩ ) − 1 ) ) = ( ⟨“ 𝑐 ”⟩ ‘ 0 )
107 106 a1i ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → ( ⟨“ 𝑐 ”⟩ ‘ ( ( ♯ ‘ ⟨“ 𝑐 ”⟩ ) − 1 ) ) = ( ⟨“ 𝑐 ”⟩ ‘ 0 ) )
108 s1fv ⊢ ( 𝑐 ∈ 𝑊 → ( ⟨“ 𝑐 ”⟩ ‘ 0 ) = 𝑐 )
109 108 adantr ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → ( ⟨“ 𝑐 ”⟩ ‘ 0 ) = 𝑐 )
110 101 107 109 3eqtrd ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → ( 𝑆 ‘ ⟨“ 𝑐 ”⟩ ) = 𝑐 )
111 fnfvelrn ⊢ ( ( 𝑆 Fn dom 𝑆 ∧ ⟨“ 𝑐 ”⟩ ∈ dom 𝑆 ) → ( 𝑆 ‘ ⟨“ 𝑐 ”⟩ ) ∈ ran 𝑆 )
112 69 99 111 sylancr ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → ( 𝑆 ‘ ⟨“ 𝑐 ”⟩ ) ∈ ran 𝑆 )
113 110 112 eqeltrrd ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → 𝑐 ∈ ran 𝑆 )
114 113 ex ⊢ ( 𝑐 ∈ 𝑊 → ( ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) → 𝑐 ∈ ran 𝑆 ) )
115 114 3ad2ant2 ⊢ ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) → ( ¬ 𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) → 𝑐 ∈ ran 𝑆 ) )
116 94 115 pm2.61d ⊢ ( ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) ∧ 𝑐 ∈ 𝑊 ∧ ( ♯ ‘ 𝑐 ) = 𝑑 ) → 𝑐 ∈ ran 𝑆 )
117 116 rabssdv ⊢ ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) → { 𝑐 ∈ 𝑊 ∣ ( ♯ ‘ 𝑐 ) = 𝑑 } ⊆ ran 𝑆 )
118 43 117 eqsstrid ⊢ ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) = 𝑑 } ⊆ ran 𝑆 )
119 41 118 unssd ⊢ ( ( 𝑑 ∈ ℕ0 ∧ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 ) → ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ∪ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) = 𝑑 } ) ⊆ ran 𝑆 )
120 119 ex ⊢ ( 𝑑 ∈ ℕ0 → ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 → ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ∪ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) = 𝑑 } ) ⊆ ran 𝑆 ) )
121 id ⊢ ( 𝑑 ∈ ℕ0 → 𝑑 ∈ ℕ0 )
122 nn0leltp1 ⊢ ( ( ( ♯ ‘ 𝑎 ) ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑎 ) ≤ 𝑑 ↔ ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) ) )
123 21 121 122 syl2anr ⊢ ( ( 𝑑 ∈ ℕ0 ∧ 𝑎 ∈ 𝑊 ) → ( ( ♯ ‘ 𝑎 ) ≤ 𝑑 ↔ ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) ) )
124 21 nn0red ⊢ ( 𝑎 ∈ 𝑊 → ( ♯ ‘ 𝑎 ) ∈ ℝ )
125 nn0re ⊢ ( 𝑑 ∈ ℕ0 → 𝑑 ∈ ℝ )
126 leloe ⊢ ( ( ( ♯ ‘ 𝑎 ) ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( ( ♯ ‘ 𝑎 ) ≤ 𝑑 ↔ ( ( ♯ ‘ 𝑎 ) < 𝑑 ∨ ( ♯ ‘ 𝑎 ) = 𝑑 ) ) )
127 124 125 126 syl2anr ⊢ ( ( 𝑑 ∈ ℕ0 ∧ 𝑎 ∈ 𝑊 ) → ( ( ♯ ‘ 𝑎 ) ≤ 𝑑 ↔ ( ( ♯ ‘ 𝑎 ) < 𝑑 ∨ ( ♯ ‘ 𝑎 ) = 𝑑 ) ) )
128 123 127 bitr3d ⊢ ( ( 𝑑 ∈ ℕ0 ∧ 𝑎 ∈ 𝑊 ) → ( ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) ↔ ( ( ♯ ‘ 𝑎 ) < 𝑑 ∨ ( ♯ ‘ 𝑎 ) = 𝑑 ) ) )
129 128 rabbidva ⊢ ( 𝑑 ∈ ℕ0 → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) } = { 𝑎 ∈ 𝑊 ∣ ( ( ♯ ‘ 𝑎 ) < 𝑑 ∨ ( ♯ ‘ 𝑎 ) = 𝑑 ) } )
130 unrab ⊢ ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ∪ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) = 𝑑 } ) = { 𝑎 ∈ 𝑊 ∣ ( ( ♯ ‘ 𝑎 ) < 𝑑 ∨ ( ♯ ‘ 𝑎 ) = 𝑑 ) }
131 129 130 eqtr4di ⊢ ( 𝑑 ∈ ℕ0 → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) } = ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ∪ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) = 𝑑 } ) )
132 131 sseq1d ⊢ ( 𝑑 ∈ ℕ0 → ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) } ⊆ ran 𝑆 ↔ ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ∪ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) = 𝑑 } ) ⊆ ran 𝑆 ) )
133 120 132 sylibrd ⊢ ( 𝑑 ∈ ℕ0 → ( { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < 𝑑 } ⊆ ran 𝑆 → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( 𝑑 + 1 ) } ⊆ ran 𝑆 ) )
134 30 33 36 39 40 133 nn0ind ⊢ ( ( ( ♯ ‘ 𝑐 ) + 1 ) ∈ ℕ0 → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( ( ♯ ‘ 𝑐 ) + 1 ) } ⊆ ran 𝑆 )
135 17 18 134 3syl ⊢ ( 𝑐 ∈ 𝑊 → { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( ( ♯ ‘ 𝑐 ) + 1 ) } ⊆ ran 𝑆 )
136 fveq2 ⊢ ( 𝑎 = 𝑐 → ( ♯ ‘ 𝑎 ) = ( ♯ ‘ 𝑐 ) )
137 136 breq1d ⊢ ( 𝑎 = 𝑐 → ( ( ♯ ‘ 𝑎 ) < ( ( ♯ ‘ 𝑐 ) + 1 ) ↔ ( ♯ ‘ 𝑐 ) < ( ( ♯ ‘ 𝑐 ) + 1 ) ) )
138 id ⊢ ( 𝑐 ∈ 𝑊 → 𝑐 ∈ 𝑊 )
139 17 nn0red ⊢ ( 𝑐 ∈ 𝑊 → ( ♯ ‘ 𝑐 ) ∈ ℝ )
140 139 ltp1d ⊢ ( 𝑐 ∈ 𝑊 → ( ♯ ‘ 𝑐 ) < ( ( ♯ ‘ 𝑐 ) + 1 ) )
141 137 138 140 elrabd ⊢ ( 𝑐 ∈ 𝑊 → 𝑐 ∈ { 𝑎 ∈ 𝑊 ∣ ( ♯ ‘ 𝑎 ) < ( ( ♯ ‘ 𝑐 ) + 1 ) } )
142 135 141 sseldd ⊢ ( 𝑐 ∈ 𝑊 → 𝑐 ∈ ran 𝑆 )
143 142 ssriv ⊢ 𝑊 ⊆ ran 𝑆
144 12 143 eqssi ⊢ ran 𝑆 = 𝑊
145 dffo2 ⊢ ( 𝑆 : dom 𝑆 –onto→ 𝑊 ↔ ( 𝑆 : dom 𝑆 ⟶ 𝑊 ∧ ran 𝑆 = 𝑊 ) )
146 10 144 145 mpbir2an ⊢ 𝑆 : dom 𝑆 –onto→ 𝑊