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

Theorem efgsfo 19420
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 19410 . . 3 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
87fdmi 6650 . . . 4 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
98feq2i 6630 . . 3 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
107, 9mpbir 230 . 2 𝑆:dom 𝑆𝑊
11 frn 6645 . . . 4 (𝑆:dom 𝑆𝑊 → ran 𝑆𝑊)
1210, 11ax-mp 5 . . 3 ran 𝑆𝑊
13 fviss 6885 . . . . . . . . 9 ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
141, 13eqsstri 3965 . . . . . . . 8 𝑊 ⊆ Word (𝐼 × 2o)
1514sseli 3927 . . . . . . 7 (𝑐𝑊𝑐 ∈ Word (𝐼 × 2o))
16 lencl 14315 . . . . . . 7 (𝑐 ∈ Word (𝐼 × 2o) → (♯‘𝑐) ∈ ℕ0)
1715, 16syl 17 . . . . . 6 (𝑐𝑊 → (♯‘𝑐) ∈ ℕ0)
18 peano2nn0 12353 . . . . . 6 ((♯‘𝑐) ∈ ℕ0 → ((♯‘𝑐) + 1) ∈ ℕ0)
1914sseli 3927 . . . . . . . . . . . 12 (𝑎𝑊𝑎 ∈ Word (𝐼 × 2o))
20 lencl 14315 . . . . . . . . . . . 12 (𝑎 ∈ Word (𝐼 × 2o) → (♯‘𝑎) ∈ ℕ0)
2119, 20syl 17 . . . . . . . . . . 11 (𝑎𝑊 → (♯‘𝑎) ∈ ℕ0)
22 nn0nlt0 12339 . . . . . . . . . . . 12 ((♯‘𝑎) ∈ ℕ0 → ¬ (♯‘𝑎) < 0)
23 breq2 5091 . . . . . . . . . . . . 13 (𝑏 = 0 → ((♯‘𝑎) < 𝑏 ↔ (♯‘𝑎) < 0))
2423notbid 317 . . . . . . . . . . . 12 (𝑏 = 0 → (¬ (♯‘𝑎) < 𝑏 ↔ ¬ (♯‘𝑎) < 0))
2522, 24syl5ibr 245 . . . . . . . . . . 11 (𝑏 = 0 → ((♯‘𝑎) ∈ ℕ0 → ¬ (♯‘𝑎) < 𝑏))
2621, 25syl5 34 . . . . . . . . . 10 (𝑏 = 0 → (𝑎𝑊 → ¬ (♯‘𝑎) < 𝑏))
2726ralrimiv 3139 . . . . . . . . 9 (𝑏 = 0 → ∀𝑎𝑊 ¬ (♯‘𝑎) < 𝑏)
28 rabeq0 4329 . . . . . . . . 9 ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = ∅ ↔ ∀𝑎𝑊 ¬ (♯‘𝑎) < 𝑏)
2927, 28sylibr 233 . . . . . . . 8 (𝑏 = 0 → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = ∅)
3029sseq1d 3962 . . . . . . 7 (𝑏 = 0 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ ∅ ⊆ ran 𝑆))
31 breq2 5091 . . . . . . . . 9 (𝑏 = 𝑑 → ((♯‘𝑎) < 𝑏 ↔ (♯‘𝑎) < 𝑑))
3231rabbidv 3412 . . . . . . . 8 (𝑏 = 𝑑 → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑})
3332sseq1d 3962 . . . . . . 7 (𝑏 = 𝑑 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆))
34 breq2 5091 . . . . . . . . 9 (𝑏 = (𝑑 + 1) → ((♯‘𝑎) < 𝑏 ↔ (♯‘𝑎) < (𝑑 + 1)))
3534rabbidv 3412 . . . . . . . 8 (𝑏 = (𝑑 + 1) → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)})
3635sseq1d 3962 . . . . . . 7 (𝑏 = (𝑑 + 1) → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆))
37 breq2 5091 . . . . . . . . 9 (𝑏 = ((♯‘𝑐) + 1) → ((♯‘𝑎) < 𝑏 ↔ (♯‘𝑎) < ((♯‘𝑐) + 1)))
3837rabbidv 3412 . . . . . . . 8 (𝑏 = ((♯‘𝑐) + 1) → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} = {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)})
3938sseq1d 3962 . . . . . . 7 (𝑏 = ((♯‘𝑐) + 1) → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)} ⊆ ran 𝑆))
40 0ss 4341 . . . . . . 7 ∅ ⊆ ran 𝑆
41 simpr 485 . . . . . . . . . 10 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆)
42 fveqeq2 6821 . . . . . . . . . . . 12 (𝑎 = 𝑐 → ((♯‘𝑎) = 𝑑 ↔ (♯‘𝑐) = 𝑑))
4342cbvrabv 3414 . . . . . . . . . . 11 {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑} = {𝑐𝑊 ∣ (♯‘𝑐) = 𝑑}
44 eliun 4941 . . . . . . . . . . . . . . 15 (𝑐 𝑥𝑊 ran (𝑇𝑥) ↔ ∃𝑥𝑊 𝑐 ∈ ran (𝑇𝑥))
45 fveq2 6812 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑏 → (𝑇𝑥) = (𝑇𝑏))
4645rneqd 5867 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑏 → ran (𝑇𝑥) = ran (𝑇𝑏))
4746eleq2d 2823 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑏 → (𝑐 ∈ ran (𝑇𝑥) ↔ 𝑐 ∈ ran (𝑇𝑏)))
4847cbvrexvw 3223 . . . . . . . . . . . . . . 15 (∃𝑥𝑊 𝑐 ∈ ran (𝑇𝑥) ↔ ∃𝑏𝑊 𝑐 ∈ ran (𝑇𝑏))
4944, 48bitri 274 . . . . . . . . . . . . . 14 (𝑐 𝑥𝑊 ran (𝑇𝑥) ↔ ∃𝑏𝑊 𝑐 ∈ ran (𝑇𝑏))
50 simpl1r 1224 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆)
51 fveq2 6812 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑏 → (♯‘𝑎) = (♯‘𝑏))
5251breq1d 5097 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑏 → ((♯‘𝑎) < 𝑑 ↔ (♯‘𝑏) < 𝑑))
53 simprl 768 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏𝑊)
5414, 53sselid 3929 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏 ∈ Word (𝐼 × 2o))
55 lencl 14315 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ Word (𝐼 × 2o) → (♯‘𝑏) ∈ ℕ0)
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑏) ∈ ℕ0)
5756nn0red 12374 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑏) ∈ ℝ)
58 2rp 12815 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ+
59 ltaddrp 12847 . . . . . . . . . . . . . . . . . . . . 21 (((♯‘𝑏) ∈ ℝ ∧ 2 ∈ ℝ+) → (♯‘𝑏) < ((♯‘𝑏) + 2))
6057, 58, 59sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑏) < ((♯‘𝑏) + 2))
611, 2, 3, 4efgtlen 19407 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) → (♯‘𝑐) = ((♯‘𝑏) + 2))
6261adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑐) = ((♯‘𝑏) + 2))
63 simpl3 1192 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑐) = 𝑑)
6462, 63eqtr3d 2779 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → ((♯‘𝑏) + 2) = 𝑑)
6560, 64breqtrd 5113 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → (♯‘𝑏) < 𝑑)
6652, 53, 65elrabd 3636 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏 ∈ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑})
6750, 66sseldd 3932 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑏 ∈ ran 𝑆)
68 ffn 6638 . . . . . . . . . . . . . . . . . . 19 (𝑆:dom 𝑆𝑊𝑆 Fn dom 𝑆)
6910, 68ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑆 Fn dom 𝑆
70 fvelrnb 6870 . . . . . . . . . . . . . . . . . 18 (𝑆 Fn dom 𝑆 → (𝑏 ∈ ran 𝑆 ↔ ∃𝑜 ∈ dom 𝑆(𝑆𝑜) = 𝑏))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ ran 𝑆 ↔ ∃𝑜 ∈ dom 𝑆(𝑆𝑜) = 𝑏)
7267, 71sylib 217 . . . . . . . . . . . . . . . 16 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → ∃𝑜 ∈ dom 𝑆(𝑆𝑜) = 𝑏)
73 simprrl 778 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑜 ∈ dom 𝑆)
741, 2, 3, 4, 5, 6efgsdm 19411 . . . . . . . . . . . . . . . . . . . . 21 (𝑜 ∈ dom 𝑆 ↔ (𝑜 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝑜‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝑜))(𝑜𝑖) ∈ ran (𝑇‘(𝑜‘(𝑖 − 1)))))
7574simp1bi 1144 . . . . . . . . . . . . . . . . . . . 20 (𝑜 ∈ dom 𝑆𝑜 ∈ (Word 𝑊 ∖ {∅}))
76 eldifi 4072 . . . . . . . . . . . . . . . . . . . 20 (𝑜 ∈ (Word 𝑊 ∖ {∅}) → 𝑜 ∈ Word 𝑊)
7773, 75, 763syl 18 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑜 ∈ Word 𝑊)
78 simpl2 1191 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐𝑊)
79 simprlr 777 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐 ∈ ran (𝑇𝑏))
80 simprrr 779 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑆𝑜) = 𝑏)
8180fveq2d 6816 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑇‘(𝑆𝑜)) = (𝑇𝑏))
8281rneqd 5867 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → ran (𝑇‘(𝑆𝑜)) = ran (𝑇𝑏))
8379, 82eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐 ∈ ran (𝑇‘(𝑆𝑜)))
841, 2, 3, 4, 5, 6efgsp1 19418 . . . . . . . . . . . . . . . . . . . 20 ((𝑜 ∈ dom 𝑆𝑐 ∈ ran (𝑇‘(𝑆𝑜))) → (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆)
8573, 83, 84syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆)
861, 2, 3, 4, 5, 6efgsval2 19414 . . . . . . . . . . . . . . . . . . 19 ((𝑜 ∈ Word 𝑊𝑐𝑊 ∧ (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) = 𝑐)
8777, 78, 85, 86syl3anc 1370 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) = 𝑐)
88 fnfvelrn 6998 . . . . . . . . . . . . . . . . . . 19 ((𝑆 Fn dom 𝑆 ∧ (𝑜 ++ ⟨“𝑐”⟩) ∈ dom 𝑆) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) ∈ ran 𝑆)
8969, 85, 88sylancr 587 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → (𝑆‘(𝑜 ++ ⟨“𝑐”⟩)) ∈ ran 𝑆)
9087, 89eqeltrrd 2839 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ ((𝑏𝑊𝑐 ∈ ran (𝑇𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏))) → 𝑐 ∈ ran 𝑆)
9190anassrs 468 . . . . . . . . . . . . . . . 16 (((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆𝑜) = 𝑏)) → 𝑐 ∈ ran 𝑆)
9272, 91rexlimddv 3155 . . . . . . . . . . . . . . 15 ((((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) ∧ (𝑏𝑊𝑐 ∈ ran (𝑇𝑏))) → 𝑐 ∈ ran 𝑆)
9392rexlimdvaa 3150 . . . . . . . . . . . . . 14 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) → (∃𝑏𝑊 𝑐 ∈ ran (𝑇𝑏) → 𝑐 ∈ ran 𝑆))
9449, 93biimtrid 241 . . . . . . . . . . . . 13 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) → (𝑐 𝑥𝑊 ran (𝑇𝑥) → 𝑐 ∈ ran 𝑆))
95 eldif 3907 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ (𝑊 𝑥𝑊 ran (𝑇𝑥)) ↔ (𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)))
965eleq2i 2829 . . . . . . . . . . . . . . . . . . . 20 (𝑐𝐷𝑐 ∈ (𝑊 𝑥𝑊 ran (𝑇𝑥)))
971, 2, 3, 4, 5, 6efgs1 19416 . . . . . . . . . . . . . . . . . . . 20 (𝑐𝐷 → ⟨“𝑐”⟩ ∈ dom 𝑆)
9896, 97sylbir 234 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ (𝑊 𝑥𝑊 ran (𝑇𝑥)) → ⟨“𝑐”⟩ ∈ dom 𝑆)
9995, 98sylbir 234 . . . . . . . . . . . . . . . . . 18 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → ⟨“𝑐”⟩ ∈ dom 𝑆)
1001, 2, 3, 4, 5, 6efgsval 19412 . . . . . . . . . . . . . . . . . 18 (⟨“𝑐”⟩ ∈ dom 𝑆 → (𝑆‘⟨“𝑐”⟩) = (⟨“𝑐”⟩‘((♯‘⟨“𝑐”⟩) − 1)))
10199, 100syl 17 . . . . . . . . . . . . . . . . 17 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (𝑆‘⟨“𝑐”⟩) = (⟨“𝑐”⟩‘((♯‘⟨“𝑐”⟩) − 1)))
102 s1len 14390 . . . . . . . . . . . . . . . . . . . . 21 (♯‘⟨“𝑐”⟩) = 1
103102oveq1i 7327 . . . . . . . . . . . . . . . . . . . 20 ((♯‘⟨“𝑐”⟩) − 1) = (1 − 1)
104 1m1e0 12125 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
105103, 104eqtri 2765 . . . . . . . . . . . . . . . . . . 19 ((♯‘⟨“𝑐”⟩) − 1) = 0
106105fveq2i 6815 . . . . . . . . . . . . . . . . . 18 (⟨“𝑐”⟩‘((♯‘⟨“𝑐”⟩) − 1)) = (⟨“𝑐”⟩‘0)
107106a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (⟨“𝑐”⟩‘((♯‘⟨“𝑐”⟩) − 1)) = (⟨“𝑐”⟩‘0))
108 s1fv 14394 . . . . . . . . . . . . . . . . . 18 (𝑐𝑊 → (⟨“𝑐”⟩‘0) = 𝑐)
109108adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (⟨“𝑐”⟩‘0) = 𝑐)
110101, 107, 1093eqtrd 2781 . . . . . . . . . . . . . . . 16 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (𝑆‘⟨“𝑐”⟩) = 𝑐)
111 fnfvelrn 6998 . . . . . . . . . . . . . . . . 17 ((𝑆 Fn dom 𝑆 ∧ ⟨“𝑐”⟩ ∈ dom 𝑆) → (𝑆‘⟨“𝑐”⟩) ∈ ran 𝑆)
11269, 99, 111sylancr 587 . . . . . . . . . . . . . . . 16 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → (𝑆‘⟨“𝑐”⟩) ∈ ran 𝑆)
113110, 112eqeltrrd 2839 . . . . . . . . . . . . . . 15 ((𝑐𝑊 ∧ ¬ 𝑐 𝑥𝑊 ran (𝑇𝑥)) → 𝑐 ∈ ran 𝑆)
114113ex 413 . . . . . . . . . . . . . 14 (𝑐𝑊 → (¬ 𝑐 𝑥𝑊 ran (𝑇𝑥) → 𝑐 ∈ ran 𝑆))
1151143ad2ant2 1133 . . . . . . . . . . . . 13 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) → (¬ 𝑐 𝑥𝑊 ran (𝑇𝑥) → 𝑐 ∈ ran 𝑆))
11694, 115pm2.61d 179 . . . . . . . . . . . 12 (((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐𝑊 ∧ (♯‘𝑐) = 𝑑) → 𝑐 ∈ ran 𝑆)
117116rabssdv 4019 . . . . . . . . . . 11 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑐𝑊 ∣ (♯‘𝑐) = 𝑑} ⊆ ran 𝑆)
11843, 117eqsstrid 3979 . . . . . . . . . 10 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑} ⊆ ran 𝑆)
11941, 118unssd 4131 . . . . . . . . 9 ((𝑑 ∈ ℕ0 ∧ {𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆) → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}) ⊆ ran 𝑆)
120119ex 413 . . . . . . . 8 (𝑑 ∈ ℕ0 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}) ⊆ ran 𝑆))
121 id 22 . . . . . . . . . . . . 13 (𝑑 ∈ ℕ0𝑑 ∈ ℕ0)
122 nn0leltp1 12459 . . . . . . . . . . . . 13 (((♯‘𝑎) ∈ ℕ0𝑑 ∈ ℕ0) → ((♯‘𝑎) ≤ 𝑑 ↔ (♯‘𝑎) < (𝑑 + 1)))
12321, 121, 122syl2anr 597 . . . . . . . . . . . 12 ((𝑑 ∈ ℕ0𝑎𝑊) → ((♯‘𝑎) ≤ 𝑑 ↔ (♯‘𝑎) < (𝑑 + 1)))
12421nn0red 12374 . . . . . . . . . . . . 13 (𝑎𝑊 → (♯‘𝑎) ∈ ℝ)
125 nn0re 12322 . . . . . . . . . . . . 13 (𝑑 ∈ ℕ0𝑑 ∈ ℝ)
126 leloe 11141 . . . . . . . . . . . . 13 (((♯‘𝑎) ∈ ℝ ∧ 𝑑 ∈ ℝ) → ((♯‘𝑎) ≤ 𝑑 ↔ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)))
127124, 125, 126syl2anr 597 . . . . . . . . . . . 12 ((𝑑 ∈ ℕ0𝑎𝑊) → ((♯‘𝑎) ≤ 𝑑 ↔ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)))
128123, 127bitr3d 280 . . . . . . . . . . 11 ((𝑑 ∈ ℕ0𝑎𝑊) → ((♯‘𝑎) < (𝑑 + 1) ↔ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)))
129128rabbidva 3411 . . . . . . . . . 10 (𝑑 ∈ ℕ0 → {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} = {𝑎𝑊 ∣ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)})
130 unrab 4250 . . . . . . . . . 10 ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}) = {𝑎𝑊 ∣ ((♯‘𝑎) < 𝑑 ∨ (♯‘𝑎) = 𝑑)}
131129, 130eqtr4di 2795 . . . . . . . . 9 (𝑑 ∈ ℕ0 → {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} = ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}))
132131sseq1d 3962 . . . . . . . 8 (𝑑 ∈ ℕ0 → ({𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆 ↔ ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ∪ {𝑎𝑊 ∣ (♯‘𝑎) = 𝑑}) ⊆ ran 𝑆))
133120, 132sylibrd 258 . . . . . . 7 (𝑑 ∈ ℕ0 → ({𝑎𝑊 ∣ (♯‘𝑎) < 𝑑} ⊆ ran 𝑆 → {𝑎𝑊 ∣ (♯‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆))
13430, 33, 36, 39, 40, 133nn0ind 12495 . . . . . 6 (((♯‘𝑐) + 1) ∈ ℕ0 → {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)} ⊆ ran 𝑆)
13517, 18, 1343syl 18 . . . . 5 (𝑐𝑊 → {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)} ⊆ ran 𝑆)
136 fveq2 6812 . . . . . . 7 (𝑎 = 𝑐 → (♯‘𝑎) = (♯‘𝑐))
137136breq1d 5097 . . . . . 6 (𝑎 = 𝑐 → ((♯‘𝑎) < ((♯‘𝑐) + 1) ↔ (♯‘𝑐) < ((♯‘𝑐) + 1)))
138 id 22 . . . . . 6 (𝑐𝑊𝑐𝑊)
13917nn0red 12374 . . . . . . 7 (𝑐𝑊 → (♯‘𝑐) ∈ ℝ)
140139ltp1d 11985 . . . . . 6 (𝑐𝑊 → (♯‘𝑐) < ((♯‘𝑐) + 1))
141137, 138, 140elrabd 3636 . . . . 5 (𝑐𝑊𝑐 ∈ {𝑎𝑊 ∣ (♯‘𝑎) < ((♯‘𝑐) + 1)})
142135, 141sseldd 3932 . . . 4 (𝑐𝑊𝑐 ∈ ran 𝑆)
143142ssriv 3935 . . 3 𝑊 ⊆ ran 𝑆
14412, 143eqssi 3947 . 2 ran 𝑆 = 𝑊
145 dffo2 6730 . 2 (𝑆:dom 𝑆onto𝑊 ↔ (𝑆:dom 𝑆𝑊 ∧ ran 𝑆 = 𝑊))
14610, 144, 145mpbir2an 708 1 𝑆:dom 𝑆onto𝑊
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1540  wcel 2105  wral 3062  wrex 3071  {crab 3404  cdif 3894  cun 3895  wss 3897  c0 4267  {csn 4571  cop 4577  cotp 4579   ciun 4937   class class class wbr 5087  cmpt 5170   I cid 5506   × cxp 5606  dom cdm 5608  ran crn 5609   Fn wfn 6461  wf 6462  ontowfo 6464  cfv 6466  (class class class)co 7317  cmpo 7319  1oc1o 8339  2oc2o 8340  cr 10950  0cc0 10951  1c1 10952   + caddc 10954   < clt 11089  cle 11090  cmin 11285  2c2 12108  0cn0 12313  +crp 12810  ...cfz 13319  ..^cfzo 13462  chash 14124  Word cword 14296   ++ cconcat 14352  ⟨“cs1 14379   splice csplice 14541  ⟨“cs2 14633   ~FG cefg 19387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-ot 4580  df-uni 4851  df-int 4893  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-om 7760  df-1st 7878  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-2o 8347  df-er 8548  df-map 8667  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-card 9775  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-nn 12054  df-2 12116  df-n0 12314  df-xnn0 12386  df-z 12400  df-uz 12663  df-rp 12811  df-fz 13320  df-fzo 13463  df-hash 14125  df-word 14297  df-concat 14353  df-s1 14380  df-substr 14433  df-pfx 14463  df-splice 14542  df-s2 14640
This theorem is referenced by:  efgredlemc  19426  efgrelexlemb  19431  efgredeu  19433  efgred2  19434
  Copyright terms: Public domain W3C validator