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

Theorem efgsfo 19711
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.)
Hypotheses
Ref Expression
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
Ref Expression
efgsfo 𝑆:dom 𝑆onto𝑊
Distinct variable groups:   𝑦,𝑧   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧,𝑚,𝑥   𝑚,𝑀   𝑥,𝑛,𝑀,𝑡,𝑣,𝑤   𝑘,𝑚,𝑡,𝑥,𝑇   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ,𝑚,𝑡,𝑥,𝑦,𝑧   𝑚,𝐼,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑚,𝑡
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐼(𝑘)   𝑀(𝑦,𝑧,𝑘)

Proof of Theorem efgsfo
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑖 𝑜 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . . 4 𝑊 = ( I ‘Word (𝐼 × 2o))
2 efgval.r . . . 4 = ( ~FG𝐼)
3 efgval2.m . . . 4 𝑀 = (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)
4 efgval2.t . . . 4 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
5 efgred.d . . . 4 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
6 efgred.s . . . 4 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
71, 2, 3, 4, 5, 6efgsf 19701 . . 3 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
87fdmi 6734 . . . 4 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
98feq2i 6715 . . 3 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
107, 9mpbir 230 . 2 𝑆:dom 𝑆𝑊
11 frn 6730 . . . 4 (𝑆:dom 𝑆𝑊 → ran 𝑆𝑊)
1210, 11ax-mp 5 . . 3 ran 𝑆𝑊
13 fviss 6974 . . . . . . . . 9 ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
141, 13eqsstri 4011 . . . . . . . 8 𝑊 ⊆ Word (𝐼 × 2o)
1514sseli 3972 . . . . . . 7 (𝑐𝑊𝑐 ∈ Word (𝐼 × 2o))
16 lencl 14524 . . . . . . 7 (𝑐 ∈ Word (𝐼 × 2o) → (♯‘𝑐) ∈ ℕ0)
1715, 16syl 17 . . . . . 6 (𝑐𝑊 → (♯‘𝑐) ∈ ℕ0)
18 peano2nn0 12550 . . . . . 6 ((♯‘𝑐) ∈ ℕ0 → ((♯‘𝑐) + 1) ∈ ℕ0)
1914sseli 3972 . . . . . . . . . . . 12 (𝑎𝑊𝑎 ∈ Word (𝐼 × 2o))
20 lencl 14524 . . . . . . . . . . . 12 (𝑎 ∈ Word (𝐼 × 2o) → (♯‘𝑎) ∈ ℕ0)
2119, 20syl 17 . . . . . . . . . . 11 (𝑎𝑊 → (♯‘𝑎) ∈ ℕ0)
22 nn0nlt0 12536 . . . . . . . . . . . 12 ((♯‘𝑎) ∈ ℕ0 → ¬ (♯‘𝑎) < 0)
23 breq2 5153 . . . . . . . . . . . . 13 (𝑏 = 0 → ((♯‘𝑎) < 𝑏 ↔ (♯‘𝑎) < 0))
2423notbid 317 . . . . . . . . . . . 12 (𝑏 = 0 → (¬ (♯‘𝑎) < 𝑏 ↔ ¬ (♯‘𝑎) < 0))
2522, 24imbitrrid 245 . . . . . . . . . . 11 (𝑏 = 0 → ((♯‘𝑎) ∈ ℕ0 → ¬ (♯‘𝑎) < 𝑏))
2621, 25syl5 34 . . . . . . . . . 10 (𝑏 = 0 → (𝑎𝑊 → ¬ (♯‘𝑎) < 𝑏))
2726ralrimiv 3134 . . . . . . . . 9 (𝑏 = 0 → ∀𝑎𝑊 ¬ (♯‘𝑎) < 𝑏)
28 rabeq0 4386 . . . . . . . . 9 ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = ∅ ↔ ∀𝑎𝑊 ¬ (♯‘𝑎) < 𝑏)
2927, 28sylibr 233 . . . . . . . 8 (𝑏 = 0 → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = ∅)
3029sseq1d 4008 . . . . . . 7 (𝑏 = 0 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ ∅ ⊆ ran 𝑆))
31 breq2 5153 . . . . . . . . 9 (𝑏 = 𝑑 → ((♯‘𝑎) < 𝑏 ↔ (♯‘𝑎) < 𝑑))
3231rabbidv 3426 . . . . . . . 8 (𝑏 = 𝑑 → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑})
3332sseq1d 4008 . . . . . . 7 (𝑏 = 𝑑 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆))
34 breq2 5153 . . . . . . . . 9 (𝑏 = (𝑑 + 1) → ((♯‘𝑎) < 𝑏 ↔ (♯‘𝑎) < (𝑑 + 1)))
3534rabbidv 3426 . . . . . . . 8 (𝑏 = (𝑑 + 1) → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)})
3635sseq1d 4008 . . . . . . 7 (𝑏 = (𝑑 + 1) → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆))
37 breq2 5153 . . . . . . . . 9 (𝑏 = ((♯‘𝑐) + 1) → ((♯‘𝑎) < 𝑏 ↔ (♯‘𝑎) < ((♯‘𝑐) + 1)))
3837rabbidv 3426 . . . . . . . 8 (𝑏 = ((♯‘𝑐) + 1) → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)})
3938sseq1d 4008 . . . . . . 7 (𝑏 = ((♯‘𝑐) + 1) → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)} ⊆ ran 𝑆))
40 0ss 4398 . . . . . . 7 ∅ ⊆ ran 𝑆
41 simpr 483 . . . . . . . . . 10 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆)
42 fveqeq2 6905 . . . . . . . . . . . 12 (𝑎 = 𝑐 → ((♯‘𝑎) = 𝑑 ↔ (♯‘𝑐) = 𝑑))
4342cbvrabv 3429 . . . . . . . . . . 11 {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑} = {𝑐𝑊 ∣ (♯‘𝑐) = 𝑑}
44 eliun 5001 . . . . . . . . . . . . . . 15 (𝑐 𝑥𝑊 ran (𝑇𝑥) ↔ ∃𝑥𝑊 𝑐 ∈ ran (𝑇𝑥))
45 fveq2 6896 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑏 → (𝑇𝑥) = (𝑇𝑏))
4645rneqd 5940 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑏 → ran (𝑇𝑥) = ran (𝑇𝑏))
4746eleq2d 2811 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑏 → (𝑐 ∈ ran (𝑇𝑥) ↔ 𝑐 ∈ ran (𝑇𝑏)))
4847cbvrexvw 3225 . . . . . . . . . . . . . . 15 (∃𝑥𝑊 𝑐 ∈ ran (𝑇𝑥) ↔ ∃𝑏𝑊 𝑐 ∈ ran (𝑇𝑏))
4944, 48bitri 274 . . . . . . . . . . . . . 14 (𝑐 𝑥𝑊 ran (𝑇𝑥) ↔ ∃𝑏𝑊 𝑐 ∈ ran (𝑇𝑏))
50 simpl1r 1222 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆)
51 fveq2 6896 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑏 → (♯‘𝑎) = (♯‘𝑏))
5251breq1d 5159 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → ((♯‘𝑎) < 𝑑 ↔ (♯‘𝑏) < 𝑑))
53 simprl 769 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏𝑊)
5414, 53sselid 3974 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏 ∈ Word (𝐼 × 2o))
55 lencl 14524 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ Word (𝐼 × 2o) → (♯‘𝑏) ∈ ℕ0)
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑏) ∈ ℕ0)
5756nn0red 12571 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑏) ∈ ℝ)
58 2rp 13019 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ+
59 ltaddrp 13051 . . . . . . . . . . . . . . . . . . . . 21 (((♯‘𝑏) ∈ ℝ ∧ 2 ∈ ℝ+) → (♯‘𝑏) < ((♯‘𝑏) + 2))
6057, 58, 59sylancl 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑏) < ((♯‘𝑏) + 2))
611, 2, 3, 4efgtlen 19698 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) → (♯‘𝑐) = ((♯‘𝑏) + 2))
6261adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑐) = ((♯‘𝑏) + 2))
63 simpl3 1190 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑐) = 𝑑)
6462, 63eqtr3d 2767 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → ((♯‘𝑏) + 2) = 𝑑)
6560, 64breqtrd 5175 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑏) < 𝑑)
6652, 53, 65elrabd 3681 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏 ∈ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑})
6750, 66sseldd 3977 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏 ∈ ran 𝑆)
68 ffn 6723 . . . . . . . . . . . . . . . . . . 19 (𝑆:dom 𝑆𝑊𝑆 Fn dom 𝑆)
6910, 68ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑆 Fn dom 𝑆
70 fvelrnb 6958 . . . . . . . . . . . . . . . . . 18 (𝑆 Fn dom 𝑆 → (𝑏 ∈ ran 𝑆 ↔ ∃𝑜 ∈ dom 𝑆(𝑆𝑜) = 𝑏))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ ran 𝑆 ↔ ∃𝑜 ∈ dom 𝑆(𝑆𝑜) = 𝑏)
7267, 71sylib 217 . . . . . . . . . . . . . . . 16 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → ∃𝑜 ∈ dom 𝑆(𝑆𝑜) = 𝑏)
73 simprrl 779 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑜 ∈ dom 𝑆)
741, 2, 3, 4, 5, 6efgsdm 19702 . . . . . . . . . . . . . . . . . . . . 21 (𝑜 ∈ dom 𝑆 ↔ (𝑜 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝑜‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝑜))(𝑜𝑖) ∈ ran (𝑇‘(𝑜‘(𝑖 − 1)))))
7574simp1bi 1142 . . . . . . . . . . . . . . . . . . . 20 (𝑜 ∈ dom 𝑆𝑜 ∈ (Word 𝑊 ∖ {∅}))
76 eldifi 4123 . . . . . . . . . . . . . . . . . . . 20 (𝑜 ∈ (Word 𝑊 ∖ {∅}) → 𝑜 ∈ Word 𝑊)
7773, 75, 763syl 18 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑜 ∈ Word 𝑊)
78 simpl2 1189 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐𝑊)
79 simprlr 778 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐 ∈ ran (𝑇𝑏))
80 simprrr 780 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑆𝑜) = 𝑏)
8180fveq2d 6900 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑇‘(𝑆𝑜)) = (𝑇𝑏))
8281rneqd 5940 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → ran (𝑇‘(𝑆𝑜)) = ran (𝑇𝑏))
8379, 82eleqtrrd 2828 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐 ∈ ran (𝑇‘(𝑆𝑜)))
841, 2, 3, 4, 5, 6efgsp1 19709 . . . . . . . . . . . . . . . . . . . 20 ((𝑜 ∈ dom 𝑆𝑐 ∈ ran (𝑇‘(𝑆𝑜))) → (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆)
8573, 83, 84syl2anc 582 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆)
861, 2, 3, 4, 5, 6efgsval2 19705 . . . . . . . . . . . . . . . . . . 19 ((𝑜 ∈ Word 𝑊𝑐𝑊 ∧ (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) = 𝑐)
8777, 78, 85, 86syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) = 𝑐)
88 fnfvelrn 7089 . . . . . . . . . . . . . . . . . . 19 ((𝑆 Fn dom 𝑆 ∧ (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) ∈ ran 𝑆)
8969, 85, 88sylancr 585 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) ∈ ran 𝑆)
9087, 89eqeltrrd 2826 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐 ∈ ran 𝑆)
9190anassrs 466 . . . . . . . . . . . . . . . 16 (((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏)) → 𝑐 ∈ ran 𝑆)
9272, 91rexlimddv 3150 . . . . . . . . . . . . . . 15 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑐 ∈ ran 𝑆)
9392rexlimdvaa 3145 . . . . . . . . . . . . . 14 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) → (∃𝑏𝑊 𝑐 ∈ ran (𝑇𝑏) → 𝑐 ∈ ran 𝑆))
9449, 93biimtrid 241 . . . . . . . . . . . . 13 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) → (𝑐 𝑥𝑊 ran (𝑇𝑥) → 𝑐 ∈ ran 𝑆))
95 eldif 3954 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ (𝑊 𝑥𝑊 ran (𝑇𝑥)) ↔ (𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)))
965eleq2i 2817 . . . . . . . . . . . . . . . . . . . 20 (𝑐𝐷𝑐 ∈ (𝑊 𝑥𝑊 ran (𝑇𝑥)))
971, 2, 3, 4, 5, 6efgs1 19707 . . . . . . . . . . . . . . . . . . . 20 (𝑐𝐷 → ⟨“𝑐”⟩ ∈ dom 𝑆)
9896, 97sylbir 234 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ (𝑊 𝑥𝑊 ran (𝑇𝑥)) → ⟨“𝑐”⟩ ∈ dom 𝑆)
9995, 98sylbir 234 . . . . . . . . . . . . . . . . . 18 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → ⟨“𝑐”⟩ ∈ dom 𝑆)
1001, 2, 3, 4, 5, 6efgsval 19703 . . . . . . . . . . . . . . . . . 18 (⟨“𝑐”⟩ ∈ dom 𝑆 → (𝑆‘⟨“𝑐”⟩) = (⟨“𝑐”⟩‘((♯‘⟨“𝑐”⟩) − 1)))
10199, 100syl 17 . . . . . . . . . . . . . . . . 17 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (𝑆‘⟨“𝑐”⟩) = (⟨“𝑐”⟩‘((♯‘⟨“𝑐”⟩) − 1)))
102 s1len 14597 . . . . . . . . . . . . . . . . . . . . 21 (♯‘⟨“𝑐”⟩) = 1
103102oveq1i 7429 . . . . . . . . . . . . . . . . . . . 20 ((♯‘⟨“𝑐”⟩) − 1) = (1 − 1)
104 1m1e0 12322 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
105103, 104eqtri 2753 . . . . . . . . . . . . . . . . . . 19 ((♯‘⟨“𝑐”⟩) − 1) = 0
106105fveq2i 6899 . . . . . . . . . . . . . . . . . 18 (⟨“𝑐”⟩‘((♯‘⟨“𝑐”⟩) − 1)) = (⟨“𝑐”⟩‘0)
107106a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (⟨“𝑐”⟩‘((♯‘⟨“𝑐”⟩) − 1)) = (⟨“𝑐”⟩‘0))
108 s1fv 14601 . . . . . . . . . . . . . . . . . 18 (𝑐𝑊 → (⟨“𝑐”⟩‘0) = 𝑐)
109108adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (⟨“𝑐”⟩‘0) = 𝑐)
110101, 107, 1093eqtrd 2769 . . . . . . . . . . . . . . . 16 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (𝑆‘⟨“𝑐”⟩) = 𝑐)
111 fnfvelrn 7089 . . . . . . . . . . . . . . . . 17 ((𝑆 Fn dom 𝑆 ∧ ⟨“𝑐”⟩ ∈ dom 𝑆) → (𝑆‘⟨“𝑐”⟩) ∈ ran 𝑆)
11269, 99, 111sylancr 585 . . . . . . . . . . . . . . . 16 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (𝑆‘⟨“𝑐”⟩) ∈ ran 𝑆)
113110, 112eqeltrrd 2826 . . . . . . . . . . . . . . 15 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → 𝑐 ∈ ran 𝑆)
114113ex 411 . . . . . . . . . . . . . 14 (𝑐𝑊 → (¬ 𝑐 𝑥𝑊 ran (𝑇𝑥) → 𝑐 ∈ ran 𝑆))
1151143ad2ant2 1131 . . . . . . . . . . . . 13 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) → (¬ 𝑐 𝑥𝑊 ran (𝑇𝑥) → 𝑐 ∈ ran 𝑆))
11694, 115pm2.61d 179 . . . . . . . . . . . 12 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) → 𝑐 ∈ ran 𝑆)
117116rabssdv 4068 . . . . . . . . . . 11 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑐𝑊 ∣ (♯‘𝑐) = 𝑑} ⊆ ran 𝑆)
11843, 117eqsstrid 4025 . . . . . . . . . 10 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑} ⊆ ran 𝑆)
11941, 118unssd 4184 . . . . . . . . 9 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}) ⊆ ran 𝑆)
120119ex 411 . . . . . . . 8 (𝑑 ∈ ℕ0 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}) ⊆ ran 𝑆))
121 id 22 . . . . . . . . . . . . 13 (𝑑 ∈ ℕ0𝑑 ∈ ℕ0)
122 nn0leltp1 12659 . . . . . . . . . . . . 13 (((♯‘𝑎) ∈ ℕ0𝑑 ∈ ℕ0) → ((♯‘𝑎) ≤ 𝑑 ↔ (♯‘𝑎) < (𝑑 + 1)))
12321, 121, 122syl2anr 595 . . . . . . . . . . . 12 ((𝑑 ∈ ℕ0𝑎𝑊) → ((♯‘𝑎) ≤ 𝑑 ↔ (♯‘𝑎) < (𝑑 + 1)))
12421nn0red 12571 . . . . . . . . . . . . 13 (𝑎𝑊 → (♯‘𝑎) ∈ ℝ)
125 nn0re 12519 . . . . . . . . . . . . 13 (𝑑 ∈ ℕ0𝑑 ∈ ℝ)
126 leloe 11337 . . . . . . . . . . . . 13 (((♯‘𝑎) ∈ ℝ ∧ 𝑑 ∈ ℝ) → ((♯‘𝑎) ≤ 𝑑 ↔ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)))
127124, 125, 126syl2anr 595 . . . . . . . . . . . 12 ((𝑑 ∈ ℕ0𝑎𝑊) → ((♯‘𝑎) ≤ 𝑑 ↔ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)))
128123, 127bitr3d 280 . . . . . . . . . . 11 ((𝑑 ∈ ℕ0𝑎𝑊) → ((♯‘𝑎) < (𝑑 + 1) ↔ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)))
129128rabbidva 3425 . . . . . . . . . 10 (𝑑 ∈ ℕ0 → {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} = {𝑎𝑊 ∣ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)})
130 unrab 4304 . . . . . . . . . 10 ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}) = {𝑎𝑊 ∣ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)}
131129, 130eqtr4di 2783 . . . . . . . . 9 (𝑑 ∈ ℕ0 → {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} = ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}))
132131sseq1d 4008 . . . . . . . 8 (𝑑 ∈ ℕ0 → ({𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆 ↔ ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}) ⊆ ran 𝑆))
133120, 132sylibrd 258 . . . . . . 7 (𝑑 ∈ ℕ0 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆 → {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆))
13430, 33, 36, 39, 40, 133nn0ind 12695 . . . . . 6 (((♯‘𝑐) + 1) ∈ ℕ0 → {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)} ⊆ ran 𝑆)
13517, 18, 1343syl 18 . . . . 5 (𝑐𝑊 → {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)} ⊆ ran 𝑆)
136 fveq2 6896 . . . . . . 7 (𝑎 = 𝑐 → (♯‘𝑎) = (♯‘𝑐))
137136breq1d 5159 . . . . . 6 (𝑎 = 𝑐 → ((♯‘𝑎) < ((♯‘𝑐) + 1) ↔ (♯‘𝑐) < ((♯‘𝑐) + 1)))
138 id 22 . . . . . 6 (𝑐𝑊𝑐𝑊)
13917nn0red 12571 . . . . . . 7 (𝑐𝑊 → (♯‘𝑐) ∈ ℝ)
140139ltp1d 12182 . . . . . 6 (𝑐𝑊 → (♯‘𝑐) < ((♯‘𝑐) + 1))
141137, 138, 140elrabd 3681 . . . . 5 (𝑐𝑊𝑐 ∈ {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)})
142135, 141sseldd 3977 . . . 4 (𝑐𝑊𝑐 ∈ ran 𝑆)
143142ssriv 3980 . . 3 𝑊 ⊆ ran 𝑆
14412, 143eqssi 3993 . 2 ran 𝑆 = 𝑊
145 dffo2 6814 . 2 (𝑆:dom 𝑆onto𝑊 ↔ (𝑆:dom 𝑆𝑊 ∧ ran 𝑆 = 𝑊))
14610, 144, 145mpbir2an 709 1 𝑆:dom 𝑆onto𝑊
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845  w3a 1084   = wceq 1533  wcel 2098  wral 3050  wrex 3059  {crab 3418  cdif 3941  cun 3942  wss 3944  c0 4322  {csn 4630  cop 4636  cotp 4638   ciun 4997   class class class wbr 5149  cmpt 5232   I cid 5575   × cxp 5676  dom cdm 5678  ran crn 5679   Fn wfn 6544  wf 6545  ontowfo 6547  cfv 6549  (class class class)co 7419  cmpo 7421  1oc1o 8480  2oc2o 8481  cr 11144  0cc0 11145  1c1 11146   + caddc 11148   < clt 11285  cle 11286  cmin 11481  2c2 12305  0cn0 12510  +crp 13014  ...cfz 13524  ..^cfzo 13667  chash 14330  Word cword 14505   ++ cconcat 14561  ⟨“cs1 14586   splice csplice 14740  ⟨“cs2 14833   ~FG cefg 19678
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-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-ot 4639  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-card 9969  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-nn 12251  df-2 12313  df-n0 12511  df-xnn0 12583  df-z 12597  df-uz 12861  df-rp 13015  df-fz 13525  df-fzo 13668  df-hash 14331  df-word 14506  df-concat 14562  df-s1 14587  df-substr 14632  df-pfx 14662  df-splice 14741  df-s2 14840
This theorem is referenced by:  efgredlemc  19717  efgrelexlemb  19722  efgredeu  19724  efgred2  19725
  Copyright terms: Public domain W3C validator