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

Theorem efgsfo 18198
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 indexes somewhere in the sequence). (Contributed by Mario Carneiro, 27-Sep-2015.)
Hypotheses
Ref Expression
efgval.w 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
efgval.r = ( ~FG𝐼)
efgval2.m 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
efgval2.t 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 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 (𝐼 × 2𝑜))
2 efgval.r . . . 4 = ( ~FG𝐼)
3 efgval2.m . . . 4 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
4 efgval2.t . . . 4 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
5 efgred.d . . . 4 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
6 efgred.s . . . 4 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))
71, 2, 3, 4, 5, 6efgsf 18188 . . 3 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
87fdmi 6090 . . . 4 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
98feq2i 6075 . . 3 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
107, 9mpbir 221 . 2 𝑆:dom 𝑆𝑊
11 frn 6091 . . . 4 (𝑆:dom 𝑆𝑊 → ran 𝑆𝑊)
1210, 11ax-mp 5 . . 3 ran 𝑆𝑊
13 fviss 6295 . . . . . . . . 9 ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
141, 13eqsstri 3668 . . . . . . . 8 𝑊 ⊆ Word (𝐼 × 2𝑜)
1514sseli 3632 . . . . . . 7 (𝑐𝑊𝑐 ∈ Word (𝐼 × 2𝑜))
16 lencl 13356 . . . . . . 7 (𝑐 ∈ Word (𝐼 × 2𝑜) → (#‘𝑐) ∈ ℕ0)
1715, 16syl 17 . . . . . 6 (𝑐𝑊 → (#‘𝑐) ∈ ℕ0)
18 peano2nn0 11371 . . . . . 6 ((#‘𝑐) ∈ ℕ0 → ((#‘𝑐) + 1) ∈ ℕ0)
1914sseli 3632 . . . . . . . . . . . 12 (𝑎𝑊𝑎 ∈ Word (𝐼 × 2𝑜))
20 lencl 13356 . . . . . . . . . . . 12 (𝑎 ∈ Word (𝐼 × 2𝑜) → (#‘𝑎) ∈ ℕ0)
2119, 20syl 17 . . . . . . . . . . 11 (𝑎𝑊 → (#‘𝑎) ∈ ℕ0)
22 nn0nlt0 11357 . . . . . . . . . . . 12 ((#‘𝑎) ∈ ℕ0 → ¬ (#‘𝑎) < 0)
23 breq2 4689 . . . . . . . . . . . . 13 (𝑏 = 0 → ((#‘𝑎) < 𝑏 ↔ (#‘𝑎) < 0))
2423notbid 307 . . . . . . . . . . . 12 (𝑏 = 0 → (¬ (#‘𝑎) < 𝑏 ↔ ¬ (#‘𝑎) < 0))
2522, 24syl5ibr 236 . . . . . . . . . . 11 (𝑏 = 0 → ((#‘𝑎) ∈ ℕ0 → ¬ (#‘𝑎) < 𝑏))
2621, 25syl5 34 . . . . . . . . . 10 (𝑏 = 0 → (𝑎𝑊 → ¬ (#‘𝑎) < 𝑏))
2726ralrimiv 2994 . . . . . . . . 9 (𝑏 = 0 → ∀𝑎𝑊 ¬ (#‘𝑎) < 𝑏)
28 rabeq0 3990 . . . . . . . . 9 ({𝑎𝑊 ∣ (#‘𝑎) < 𝑏} = ∅ ↔ ∀𝑎𝑊 ¬ (#‘𝑎) < 𝑏)
2927, 28sylibr 224 . . . . . . . 8 (𝑏 = 0 → {𝑎𝑊 ∣ (#‘𝑎) < 𝑏} = ∅)
3029sseq1d 3665 . . . . . . 7 (𝑏 = 0 → ({𝑎𝑊 ∣ (#‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ ∅ ⊆ ran 𝑆))
31 breq2 4689 . . . . . . . . 9 (𝑏 = 𝑑 → ((#‘𝑎) < 𝑏 ↔ (#‘𝑎) < 𝑑))
3231rabbidv 3220 . . . . . . . 8 (𝑏 = 𝑑 → {𝑎𝑊 ∣ (#‘𝑎) < 𝑏} = {𝑎𝑊 ∣ (#‘𝑎) < 𝑑})
3332sseq1d 3665 . . . . . . 7 (𝑏 = 𝑑 → ({𝑎𝑊 ∣ (#‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆))
34 breq2 4689 . . . . . . . . 9 (𝑏 = (𝑑 + 1) → ((#‘𝑎) < 𝑏 ↔ (#‘𝑎) < (𝑑 + 1)))
3534rabbidv 3220 . . . . . . . 8 (𝑏 = (𝑑 + 1) → {𝑎𝑊 ∣ (#‘𝑎) < 𝑏} = {𝑎𝑊 ∣ (#‘𝑎) < (𝑑 + 1)})
3635sseq1d 3665 . . . . . . 7 (𝑏 = (𝑑 + 1) → ({𝑎𝑊 ∣ (#‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆))
37 breq2 4689 . . . . . . . . 9 (𝑏 = ((#‘𝑐) + 1) → ((#‘𝑎) < 𝑏 ↔ (#‘𝑎) < ((#‘𝑐) + 1)))
3837rabbidv 3220 . . . . . . . 8 (𝑏 = ((#‘𝑐) + 1) → {𝑎𝑊 ∣ (#‘𝑎) < 𝑏} = {𝑎𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)})
3938sseq1d 3665 . . . . . . 7 (𝑏 = ((#‘𝑐) + 1) → ({𝑎𝑊 ∣ (#‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)} ⊆ ran 𝑆))
40 0ss 4005 . . . . . . 7 ∅ ⊆ ran 𝑆
41 simpr 476 . . . . . . . . . 10 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆)
42 fveq2 6229 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → (#‘𝑎) = (#‘𝑐))
4342eqeq1d 2653 . . . . . . . . . . . 12 (𝑎 = 𝑐 → ((#‘𝑎) = 𝑑 ↔ (#‘𝑐) = 𝑑))
4443cbvrabv 3230 . . . . . . . . . . 11 {𝑎𝑊 ∣ (#‘𝑎) = 𝑑} = {𝑐𝑊 ∣ (#‘𝑐) = 𝑑}
45 eliun 4556 . . . . . . . . . . . . . . 15 (𝑐 𝑥𝑊 ran (𝑇𝑥) ↔ ∃𝑥𝑊 𝑐 ∈ ran (𝑇𝑥))
46 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑏 → (𝑇𝑥) = (𝑇𝑏))
4746rneqd 5385 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑏 → ran (𝑇𝑥) = ran (𝑇𝑏))
4847eleq2d 2716 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑏 → (𝑐 ∈ ran (𝑇𝑥) ↔ 𝑐 ∈ ran (𝑇𝑏)))
4948cbvrexv 3202 . . . . . . . . . . . . . . 15 (∃𝑥𝑊 𝑐 ∈ ran (𝑇𝑥) ↔ ∃𝑏𝑊 𝑐 ∈ ran (𝑇𝑏))
5045, 49bitri 264 . . . . . . . . . . . . . 14 (𝑐 𝑥𝑊 ran (𝑇𝑥) ↔ ∃𝑏𝑊 𝑐 ∈ ran (𝑇𝑏))
51 simpl1r 1133 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆)
52 simprl 809 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏𝑊)
5314, 52sseldi 3634 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏 ∈ Word (𝐼 × 2𝑜))
54 lencl 13356 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ Word (𝐼 × 2𝑜) → (#‘𝑏) ∈ ℕ0)
5553, 54syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (#‘𝑏) ∈ ℕ0)
5655nn0red 11390 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (#‘𝑏) ∈ ℝ)
57 2rp 11875 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ+
58 ltaddrp 11905 . . . . . . . . . . . . . . . . . . . . 21 (((#‘𝑏) ∈ ℝ ∧ 2 ∈ ℝ+) → (#‘𝑏) < ((#‘𝑏) + 2))
5956, 57, 58sylancl 695 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (#‘𝑏) < ((#‘𝑏) + 2))
601, 2, 3, 4efgtlen 18185 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) → (#‘𝑐) = ((#‘𝑏) + 2))
6160adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (#‘𝑐) = ((#‘𝑏) + 2))
62 simpl3 1086 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (#‘𝑐) = 𝑑)
6361, 62eqtr3d 2687 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → ((#‘𝑏) + 2) = 𝑑)
6459, 63breqtrd 4711 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (#‘𝑏) < 𝑑)
65 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑏 → (#‘𝑎) = (#‘𝑏))
6665breq1d 4695 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑏 → ((#‘𝑎) < 𝑑 ↔ (#‘𝑏) < 𝑑))
6766elrab 3396 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ↔ (𝑏𝑊 ∧ (#‘𝑏) < 𝑑))
6852, 64, 67sylanbrc 699 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏 ∈ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑})
6951, 68sseldd 3637 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏 ∈ ran 𝑆)
70 ffn 6083 . . . . . . . . . . . . . . . . . . 19 (𝑆:dom 𝑆𝑊𝑆 Fn dom 𝑆)
7110, 70ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑆 Fn dom 𝑆
72 fvelrnb 6282 . . . . . . . . . . . . . . . . . 18 (𝑆 Fn dom 𝑆 → (𝑏 ∈ ran 𝑆 ↔ ∃𝑜 ∈ dom 𝑆(𝑆𝑜) = 𝑏))
7371, 72ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ ran 𝑆 ↔ ∃𝑜 ∈ dom 𝑆(𝑆𝑜) = 𝑏)
7469, 73sylib 208 . . . . . . . . . . . . . . . 16 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → ∃𝑜 ∈ dom 𝑆(𝑆𝑜) = 𝑏)
75 simprrl 821 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑜 ∈ dom 𝑆)
761, 2, 3, 4, 5, 6efgsdm 18189 . . . . . . . . . . . . . . . . . . . . 21 (𝑜 ∈ dom 𝑆 ↔ (𝑜 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝑜‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝑜))(𝑜𝑖) ∈ ran (𝑇‘(𝑜‘(𝑖 − 1)))))
7776simp1bi 1096 . . . . . . . . . . . . . . . . . . . 20 (𝑜 ∈ dom 𝑆𝑜 ∈ (Word 𝑊 ∖ {∅}))
78 eldifi 3765 . . . . . . . . . . . . . . . . . . . 20 (𝑜 ∈ (Word 𝑊 ∖ {∅}) → 𝑜 ∈ Word 𝑊)
7975, 77, 783syl 18 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑜 ∈ Word 𝑊)
80 simpl2 1085 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐𝑊)
81 simprlr 820 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐 ∈ ran (𝑇𝑏))
82 simprrr 822 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑆𝑜) = 𝑏)
8382fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑇‘(𝑆𝑜)) = (𝑇𝑏))
8483rneqd 5385 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → ran (𝑇‘(𝑆𝑜)) = ran (𝑇𝑏))
8581, 84eleqtrrd 2733 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐 ∈ ran (𝑇‘(𝑆𝑜)))
861, 2, 3, 4, 5, 6efgsp1 18196 . . . . . . . . . . . . . . . . . . . 20 ((𝑜 ∈ dom 𝑆𝑐 ∈ ran (𝑇‘(𝑆𝑜))) → (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆)
8775, 85, 86syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆)
881, 2, 3, 4, 5, 6efgsval2 18192 . . . . . . . . . . . . . . . . . . 19 ((𝑜 ∈ Word 𝑊𝑐𝑊 ∧ (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) = 𝑐)
8979, 80, 87, 88syl3anc 1366 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) = 𝑐)
90 fnfvelrn 6396 . . . . . . . . . . . . . . . . . . 19 ((𝑆 Fn dom 𝑆 ∧ (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) ∈ ran 𝑆)
9171, 87, 90sylancr 696 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) ∈ ran 𝑆)
9289, 91eqeltrrd 2731 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐 ∈ ran 𝑆)
9392anassrs 681 . . . . . . . . . . . . . . . 16 (((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏)) → 𝑐 ∈ ran 𝑆)
9474, 93rexlimddv 3064 . . . . . . . . . . . . . . 15 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑐 ∈ ran 𝑆)
9594rexlimdvaa 3061 . . . . . . . . . . . . . 14 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) → (∃𝑏𝑊 𝑐 ∈ ran (𝑇𝑏) → 𝑐 ∈ ran 𝑆))
9650, 95syl5bi 232 . . . . . . . . . . . . 13 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) → (𝑐 𝑥𝑊 ran (𝑇𝑥) → 𝑐 ∈ ran 𝑆))
97 eldif 3617 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ (𝑊 𝑥𝑊 ran (𝑇𝑥)) ↔ (𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)))
985eleq2i 2722 . . . . . . . . . . . . . . . . . . . 20 (𝑐𝐷𝑐 ∈ (𝑊 𝑥𝑊 ran (𝑇𝑥)))
991, 2, 3, 4, 5, 6efgs1 18194 . . . . . . . . . . . . . . . . . . . 20 (𝑐𝐷 → ⟨“𝑐”⟩ ∈ dom 𝑆)
10098, 99sylbir 225 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ (𝑊 𝑥𝑊 ran (𝑇𝑥)) → ⟨“𝑐”⟩ ∈ dom 𝑆)
10197, 100sylbir 225 . . . . . . . . . . . . . . . . . 18 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → ⟨“𝑐”⟩ ∈ dom 𝑆)
1021, 2, 3, 4, 5, 6efgsval 18190 . . . . . . . . . . . . . . . . . 18 (⟨“𝑐”⟩ ∈ dom 𝑆 → (𝑆‘⟨“𝑐”⟩) = (⟨“𝑐”⟩‘((#‘⟨“𝑐”⟩) − 1)))
103101, 102syl 17 . . . . . . . . . . . . . . . . 17 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (𝑆‘⟨“𝑐”⟩) = (⟨“𝑐”⟩‘((#‘⟨“𝑐”⟩) − 1)))
104 s1len 13422 . . . . . . . . . . . . . . . . . . . . 21 (#‘⟨“𝑐”⟩) = 1
105104oveq1i 6700 . . . . . . . . . . . . . . . . . . . 20 ((#‘⟨“𝑐”⟩) − 1) = (1 − 1)
106 1m1e0 11127 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
107105, 106eqtri 2673 . . . . . . . . . . . . . . . . . . 19 ((#‘⟨“𝑐”⟩) − 1) = 0
108107fveq2i 6232 . . . . . . . . . . . . . . . . . 18 (⟨“𝑐”⟩‘((#‘⟨“𝑐”⟩) − 1)) = (⟨“𝑐”⟩‘0)
109108a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (⟨“𝑐”⟩‘((#‘⟨“𝑐”⟩) − 1)) = (⟨“𝑐”⟩‘0))
110 s1fv 13427 . . . . . . . . . . . . . . . . . 18 (𝑐𝑊 → (⟨“𝑐”⟩‘0) = 𝑐)
111110adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (⟨“𝑐”⟩‘0) = 𝑐)
112103, 109, 1113eqtrd 2689 . . . . . . . . . . . . . . . 16 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (𝑆‘⟨“𝑐”⟩) = 𝑐)
113 fnfvelrn 6396 . . . . . . . . . . . . . . . . 17 ((𝑆 Fn dom 𝑆 ∧ ⟨“𝑐”⟩ ∈ dom 𝑆) → (𝑆‘⟨“𝑐”⟩) ∈ ran 𝑆)
11471, 101, 113sylancr 696 . . . . . . . . . . . . . . . 16 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (𝑆‘⟨“𝑐”⟩) ∈ ran 𝑆)
115112, 114eqeltrrd 2731 . . . . . . . . . . . . . . 15 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → 𝑐 ∈ ran 𝑆)
116115ex 449 . . . . . . . . . . . . . 14 (𝑐𝑊 → (¬ 𝑐 𝑥𝑊 ran (𝑇𝑥) → 𝑐 ∈ ran 𝑆))
1171163ad2ant2 1103 . . . . . . . . . . . . 13 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) → (¬ 𝑐 𝑥𝑊 ran (𝑇𝑥) → 𝑐 ∈ ran 𝑆))
11896, 117pm2.61d 170 . . . . . . . . . . . 12 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (#‘𝑐) = 𝑑) → 𝑐 ∈ ran 𝑆)
119118rabssdv 3715 . . . . . . . . . . 11 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑐𝑊 ∣ (#‘𝑐) = 𝑑} ⊆ ran 𝑆)
12044, 119syl5eqss 3682 . . . . . . . . . 10 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑎𝑊 ∣ (#‘𝑎) = 𝑑} ⊆ ran 𝑆)
12141, 120unssd 3822 . . . . . . . . 9 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) → ({𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (#‘𝑎) = 𝑑}) ⊆ ran 𝑆)
122121ex 449 . . . . . . . 8 (𝑑 ∈ ℕ0 → ({𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆 → ({𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (#‘𝑎) = 𝑑}) ⊆ ran 𝑆))
123 id 22 . . . . . . . . . . . . 13 (𝑑 ∈ ℕ0𝑑 ∈ ℕ0)
124 nn0leltp1 11474 . . . . . . . . . . . . 13 (((#‘𝑎) ∈ ℕ0𝑑 ∈ ℕ0) → ((#‘𝑎) ≤ 𝑑 ↔ (#‘𝑎) < (𝑑 + 1)))
12521, 123, 124syl2anr 494 . . . . . . . . . . . 12 ((𝑑 ∈ ℕ0𝑎𝑊) → ((#‘𝑎) ≤ 𝑑 ↔ (#‘𝑎) < (𝑑 + 1)))
12621nn0red 11390 . . . . . . . . . . . . 13 (𝑎𝑊 → (#‘𝑎) ∈ ℝ)
127 nn0re 11339 . . . . . . . . . . . . 13 (𝑑 ∈ ℕ0𝑑 ∈ ℝ)
128 leloe 10162 . . . . . . . . . . . . 13 (((#‘𝑎) ∈ ℝ ∧ 𝑑 ∈ ℝ) → ((#‘𝑎) ≤ 𝑑 ↔ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑)))
129126, 127, 128syl2anr 494 . . . . . . . . . . . 12 ((𝑑 ∈ ℕ0𝑎𝑊) → ((#‘𝑎) ≤ 𝑑 ↔ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑)))
130125, 129bitr3d 270 . . . . . . . . . . 11 ((𝑑 ∈ ℕ0𝑎𝑊) → ((#‘𝑎) < (𝑑 + 1) ↔ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑)))
131130rabbidva 3219 . . . . . . . . . 10 (𝑑 ∈ ℕ0 → {𝑎𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} = {𝑎𝑊 ∣ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑)})
132 unrab 3931 . . . . . . . . . 10 ({𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (#‘𝑎) = 𝑑}) = {𝑎𝑊 ∣ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑)}
133131, 132syl6eqr 2703 . . . . . . . . 9 (𝑑 ∈ ℕ0 → {𝑎𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} = ({𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (#‘𝑎) = 𝑑}))
134133sseq1d 3665 . . . . . . . 8 (𝑑 ∈ ℕ0 → ({𝑎𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆 ↔ ({𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (#‘𝑎) = 𝑑}) ⊆ ran 𝑆))
135122, 134sylibrd 249 . . . . . . 7 (𝑑 ∈ ℕ0 → ({𝑎𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆 → {𝑎𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆))
13630, 33, 36, 39, 40, 135nn0ind 11510 . . . . . 6 (((#‘𝑐) + 1) ∈ ℕ0 → {𝑎𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)} ⊆ ran 𝑆)
13717, 18, 1363syl 18 . . . . 5 (𝑐𝑊 → {𝑎𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)} ⊆ ran 𝑆)
138 id 22 . . . . . 6 (𝑐𝑊𝑐𝑊)
13917nn0red 11390 . . . . . . 7 (𝑐𝑊 → (#‘𝑐) ∈ ℝ)
140139ltp1d 10992 . . . . . 6 (𝑐𝑊 → (#‘𝑐) < ((#‘𝑐) + 1))
14142breq1d 4695 . . . . . . 7 (𝑎 = 𝑐 → ((#‘𝑎) < ((#‘𝑐) + 1) ↔ (#‘𝑐) < ((#‘𝑐) + 1)))
142141elrab 3396 . . . . . 6 (𝑐 ∈ {𝑎𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)} ↔ (𝑐𝑊 ∧ (#‘𝑐) < ((#‘𝑐) + 1)))
143138, 140, 142sylanbrc 699 . . . . 5 (𝑐𝑊𝑐 ∈ {𝑎𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)})
144137, 143sseldd 3637 . . . 4 (𝑐𝑊𝑐 ∈ ran 𝑆)
145144ssriv 3640 . . 3 𝑊 ⊆ ran 𝑆
14612, 145eqssi 3652 . 2 ran 𝑆 = 𝑊
147 dffo2 6157 . 2 (𝑆:dom 𝑆onto𝑊 ↔ (𝑆:dom 𝑆𝑊 ∧ ran 𝑆 = 𝑊))
14810, 146, 147mpbir2an 975 1 𝑆:dom 𝑆onto𝑊
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  {crab 2945  cdif 3604  cun 3605  wss 3607  c0 3948  {csn 4210  cop 4216  cotp 4218   ciun 4552   class class class wbr 4685  cmpt 4762   I cid 5052   × cxp 5141  dom cdm 5143  ran crn 5144   Fn wfn 5921  wf 5922  ontowfo 5924  cfv 5926  (class class class)co 6690  cmpt2 6692  1𝑜c1o 7598  2𝑜c2o 7599  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112  cle 10113  cmin 10304  2c2 11108  0cn0 11330  +crp 11870  ...cfz 12364  ..^cfzo 12504  #chash 13157  Word cword 13323   ++ cconcat 13325  ⟨“cs1 13326   splice csplice 13328  ⟨“cs2 13632   ~FG cefg 18165
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-ot 4219  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-hash 13158  df-word 13331  df-concat 13333  df-s1 13334  df-substr 13335  df-splice 13336  df-s2 13639
This theorem is referenced by:  efgredlemc  18204  efgrelexlemb  18209  efgredeu  18211  efgred2  18212
  Copyright terms: Public domain W3C validator