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

Theorem efgsfo 19528
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 19518 . . 3 𝑆:{𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))}βŸΆπ‘Š
87fdmi 6685 . . . 4 dom 𝑆 = {𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))}
98feq2i 6665 . . 3 (𝑆:dom π‘†βŸΆπ‘Š ↔ 𝑆:{𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))}βŸΆπ‘Š)
107, 9mpbir 230 . 2 𝑆:dom π‘†βŸΆπ‘Š
11 frn 6680 . . . 4 (𝑆:dom π‘†βŸΆπ‘Š β†’ ran 𝑆 βŠ† π‘Š)
1210, 11ax-mp 5 . . 3 ran 𝑆 βŠ† π‘Š
13 fviss 6923 . . . . . . . . 9 ( I β€˜Word (𝐼 Γ— 2o)) βŠ† Word (𝐼 Γ— 2o)
141, 13eqsstri 3983 . . . . . . . 8 π‘Š βŠ† Word (𝐼 Γ— 2o)
1514sseli 3945 . . . . . . 7 (𝑐 ∈ π‘Š β†’ 𝑐 ∈ Word (𝐼 Γ— 2o))
16 lencl 14428 . . . . . . 7 (𝑐 ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜π‘) ∈ β„•0)
1715, 16syl 17 . . . . . 6 (𝑐 ∈ π‘Š β†’ (β™―β€˜π‘) ∈ β„•0)
18 peano2nn0 12460 . . . . . 6 ((β™―β€˜π‘) ∈ β„•0 β†’ ((β™―β€˜π‘) + 1) ∈ β„•0)
1914sseli 3945 . . . . . . . . . . . 12 (π‘Ž ∈ π‘Š β†’ π‘Ž ∈ Word (𝐼 Γ— 2o))
20 lencl 14428 . . . . . . . . . . . 12 (π‘Ž ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜π‘Ž) ∈ β„•0)
2119, 20syl 17 . . . . . . . . . . 11 (π‘Ž ∈ π‘Š β†’ (β™―β€˜π‘Ž) ∈ β„•0)
22 nn0nlt0 12446 . . . . . . . . . . . 12 ((β™―β€˜π‘Ž) ∈ β„•0 β†’ Β¬ (β™―β€˜π‘Ž) < 0)
23 breq2 5114 . . . . . . . . . . . . 13 (𝑏 = 0 β†’ ((β™―β€˜π‘Ž) < 𝑏 ↔ (β™―β€˜π‘Ž) < 0))
2423notbid 318 . . . . . . . . . . . 12 (𝑏 = 0 β†’ (Β¬ (β™―β€˜π‘Ž) < 𝑏 ↔ Β¬ (β™―β€˜π‘Ž) < 0))
2522, 24syl5ibr 246 . . . . . . . . . . 11 (𝑏 = 0 β†’ ((β™―β€˜π‘Ž) ∈ β„•0 β†’ Β¬ (β™―β€˜π‘Ž) < 𝑏))
2621, 25syl5 34 . . . . . . . . . 10 (𝑏 = 0 β†’ (π‘Ž ∈ π‘Š β†’ Β¬ (β™―β€˜π‘Ž) < 𝑏))
2726ralrimiv 3143 . . . . . . . . 9 (𝑏 = 0 β†’ βˆ€π‘Ž ∈ π‘Š Β¬ (β™―β€˜π‘Ž) < 𝑏)
28 rabeq0 4349 . . . . . . . . 9 ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑏} = βˆ… ↔ βˆ€π‘Ž ∈ π‘Š Β¬ (β™―β€˜π‘Ž) < 𝑏)
2927, 28sylibr 233 . . . . . . . 8 (𝑏 = 0 β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑏} = βˆ…)
3029sseq1d 3980 . . . . . . 7 (𝑏 = 0 β†’ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑏} βŠ† ran 𝑆 ↔ βˆ… βŠ† ran 𝑆))
31 breq2 5114 . . . . . . . . 9 (𝑏 = 𝑑 β†’ ((β™―β€˜π‘Ž) < 𝑏 ↔ (β™―β€˜π‘Ž) < 𝑑))
3231rabbidv 3418 . . . . . . . 8 (𝑏 = 𝑑 β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑏} = {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑})
3332sseq1d 3980 . . . . . . 7 (𝑏 = 𝑑 β†’ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑏} βŠ† ran 𝑆 ↔ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆))
34 breq2 5114 . . . . . . . . 9 (𝑏 = (𝑑 + 1) β†’ ((β™―β€˜π‘Ž) < 𝑏 ↔ (β™―β€˜π‘Ž) < (𝑑 + 1)))
3534rabbidv 3418 . . . . . . . 8 (𝑏 = (𝑑 + 1) β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑏} = {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < (𝑑 + 1)})
3635sseq1d 3980 . . . . . . 7 (𝑏 = (𝑑 + 1) β†’ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑏} βŠ† ran 𝑆 ↔ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < (𝑑 + 1)} βŠ† ran 𝑆))
37 breq2 5114 . . . . . . . . 9 (𝑏 = ((β™―β€˜π‘) + 1) β†’ ((β™―β€˜π‘Ž) < 𝑏 ↔ (β™―β€˜π‘Ž) < ((β™―β€˜π‘) + 1)))
3837rabbidv 3418 . . . . . . . 8 (𝑏 = ((β™―β€˜π‘) + 1) β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑏} = {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < ((β™―β€˜π‘) + 1)})
3938sseq1d 3980 . . . . . . 7 (𝑏 = ((β™―β€˜π‘) + 1) β†’ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑏} βŠ† ran 𝑆 ↔ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < ((β™―β€˜π‘) + 1)} βŠ† ran 𝑆))
40 0ss 4361 . . . . . . 7 βˆ… βŠ† ran 𝑆
41 simpr 486 . . . . . . . . . 10 ((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆)
42 fveqeq2 6856 . . . . . . . . . . . 12 (π‘Ž = 𝑐 β†’ ((β™―β€˜π‘Ž) = 𝑑 ↔ (β™―β€˜π‘) = 𝑑))
4342cbvrabv 3420 . . . . . . . . . . 11 {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) = 𝑑} = {𝑐 ∈ π‘Š ∣ (β™―β€˜π‘) = 𝑑}
44 eliun 4963 . . . . . . . . . . . . . . 15 (𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯) ↔ βˆƒπ‘₯ ∈ π‘Š 𝑐 ∈ ran (π‘‡β€˜π‘₯))
45 fveq2 6847 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑏 β†’ (π‘‡β€˜π‘₯) = (π‘‡β€˜π‘))
4645rneqd 5898 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑏 β†’ ran (π‘‡β€˜π‘₯) = ran (π‘‡β€˜π‘))
4746eleq2d 2824 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑏 β†’ (𝑐 ∈ ran (π‘‡β€˜π‘₯) ↔ 𝑐 ∈ ran (π‘‡β€˜π‘)))
4847cbvrexvw 3229 . . . . . . . . . . . . . . 15 (βˆƒπ‘₯ ∈ π‘Š 𝑐 ∈ ran (π‘‡β€˜π‘₯) ↔ βˆƒπ‘ ∈ π‘Š 𝑐 ∈ ran (π‘‡β€˜π‘))
4944, 48bitri 275 . . . . . . . . . . . . . 14 (𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯) ↔ βˆƒπ‘ ∈ π‘Š 𝑐 ∈ ran (π‘‡β€˜π‘))
50 simpl1r 1226 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆)
51 fveq2 6847 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = 𝑏 β†’ (β™―β€˜π‘Ž) = (β™―β€˜π‘))
5251breq1d 5120 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = 𝑏 β†’ ((β™―β€˜π‘Ž) < 𝑑 ↔ (β™―β€˜π‘) < 𝑑))
53 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ 𝑏 ∈ π‘Š)
5414, 53sselid 3947 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ 𝑏 ∈ Word (𝐼 Γ— 2o))
55 lencl 14428 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜π‘) ∈ β„•0)
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ (β™―β€˜π‘) ∈ β„•0)
5756nn0red 12481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ (β™―β€˜π‘) ∈ ℝ)
58 2rp 12927 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ+
59 ltaddrp 12959 . . . . . . . . . . . . . . . . . . . . 21 (((β™―β€˜π‘) ∈ ℝ ∧ 2 ∈ ℝ+) β†’ (β™―β€˜π‘) < ((β™―β€˜π‘) + 2))
6057, 58, 59sylancl 587 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ (β™―β€˜π‘) < ((β™―β€˜π‘) + 2))
611, 2, 3, 4efgtlen 19515 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) β†’ (β™―β€˜π‘) = ((β™―β€˜π‘) + 2))
6261adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ (β™―β€˜π‘) = ((β™―β€˜π‘) + 2))
63 simpl3 1194 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ (β™―β€˜π‘) = 𝑑)
6462, 63eqtr3d 2779 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ ((β™―β€˜π‘) + 2) = 𝑑)
6560, 64breqtrd 5136 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ (β™―β€˜π‘) < 𝑑)
6652, 53, 65elrabd 3652 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ 𝑏 ∈ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑})
6750, 66sseldd 3950 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ 𝑏 ∈ ran 𝑆)
68 ffn 6673 . . . . . . . . . . . . . . . . . . 19 (𝑆:dom π‘†βŸΆπ‘Š β†’ 𝑆 Fn dom 𝑆)
6910, 68ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑆 Fn dom 𝑆
70 fvelrnb 6908 . . . . . . . . . . . . . . . . . 18 (𝑆 Fn dom 𝑆 β†’ (𝑏 ∈ ran 𝑆 ↔ βˆƒπ‘œ ∈ dom 𝑆(π‘†β€˜π‘œ) = 𝑏))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ ran 𝑆 ↔ βˆƒπ‘œ ∈ dom 𝑆(π‘†β€˜π‘œ) = 𝑏)
7267, 71sylib 217 . . . . . . . . . . . . . . . 16 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ βˆƒπ‘œ ∈ dom 𝑆(π‘†β€˜π‘œ) = 𝑏)
73 simprrl 780 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ π‘œ ∈ dom 𝑆)
741, 2, 3, 4, 5, 6efgsdm 19519 . . . . . . . . . . . . . . . . . . . . 21 (π‘œ ∈ dom 𝑆 ↔ (π‘œ ∈ (Word π‘Š βˆ– {βˆ…}) ∧ (π‘œβ€˜0) ∈ 𝐷 ∧ βˆ€π‘– ∈ (1..^(β™―β€˜π‘œ))(π‘œβ€˜π‘–) ∈ ran (π‘‡β€˜(π‘œβ€˜(𝑖 βˆ’ 1)))))
7574simp1bi 1146 . . . . . . . . . . . . . . . . . . . 20 (π‘œ ∈ dom 𝑆 β†’ π‘œ ∈ (Word π‘Š βˆ– {βˆ…}))
76 eldifi 4091 . . . . . . . . . . . . . . . . . . . 20 (π‘œ ∈ (Word π‘Š βˆ– {βˆ…}) β†’ π‘œ ∈ Word π‘Š)
7773, 75, 763syl 18 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ π‘œ ∈ Word π‘Š)
78 simpl2 1193 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ 𝑐 ∈ π‘Š)
79 simprlr 779 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ 𝑐 ∈ ran (π‘‡β€˜π‘))
80 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ (π‘†β€˜π‘œ) = 𝑏)
8180fveq2d 6851 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ (π‘‡β€˜(π‘†β€˜π‘œ)) = (π‘‡β€˜π‘))
8281rneqd 5898 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ ran (π‘‡β€˜(π‘†β€˜π‘œ)) = ran (π‘‡β€˜π‘))
8379, 82eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ 𝑐 ∈ ran (π‘‡β€˜(π‘†β€˜π‘œ)))
841, 2, 3, 4, 5, 6efgsp1 19526 . . . . . . . . . . . . . . . . . . . 20 ((π‘œ ∈ dom 𝑆 ∧ 𝑐 ∈ ran (π‘‡β€˜(π‘†β€˜π‘œ))) β†’ (π‘œ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆)
8573, 83, 84syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ (π‘œ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆)
861, 2, 3, 4, 5, 6efgsval2 19522 . . . . . . . . . . . . . . . . . . 19 ((π‘œ ∈ Word π‘Š ∧ 𝑐 ∈ π‘Š ∧ (π‘œ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆) β†’ (π‘†β€˜(π‘œ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑐)
8777, 78, 85, 86syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ (π‘†β€˜(π‘œ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑐)
88 fnfvelrn 7036 . . . . . . . . . . . . . . . . . . 19 ((𝑆 Fn dom 𝑆 ∧ (π‘œ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆) β†’ (π‘†β€˜(π‘œ ++ βŸ¨β€œπ‘β€βŸ©)) ∈ ran 𝑆)
8969, 85, 88sylancr 588 . . . . . . . . . . . . . . . . . 18 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ (π‘†β€˜(π‘œ ++ βŸ¨β€œπ‘β€βŸ©)) ∈ ran 𝑆)
9087, 89eqeltrrd 2839 . . . . . . . . . . . . . . . . 17 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ ((𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘)) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏))) β†’ 𝑐 ∈ ran 𝑆)
9190anassrs 469 . . . . . . . . . . . . . . . 16 (((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) ∧ (π‘œ ∈ dom 𝑆 ∧ (π‘†β€˜π‘œ) = 𝑏)) β†’ 𝑐 ∈ ran 𝑆)
9272, 91rexlimddv 3159 . . . . . . . . . . . . . . 15 ((((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) ∧ (𝑏 ∈ π‘Š ∧ 𝑐 ∈ ran (π‘‡β€˜π‘))) β†’ 𝑐 ∈ ran 𝑆)
9392rexlimdvaa 3154 . . . . . . . . . . . . . 14 (((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) β†’ (βˆƒπ‘ ∈ π‘Š 𝑐 ∈ ran (π‘‡β€˜π‘) β†’ 𝑐 ∈ ran 𝑆))
9449, 93biimtrid 241 . . . . . . . . . . . . 13 (((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) β†’ (𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯) β†’ 𝑐 ∈ ran 𝑆))
95 eldif 3925 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ (π‘Š βˆ– βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)) ↔ (𝑐 ∈ π‘Š ∧ Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)))
965eleq2i 2830 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ 𝐷 ↔ 𝑐 ∈ (π‘Š βˆ– βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)))
971, 2, 3, 4, 5, 6efgs1 19524 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ 𝐷 β†’ βŸ¨β€œπ‘β€βŸ© ∈ dom 𝑆)
9896, 97sylbir 234 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ (π‘Š βˆ– βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)) β†’ βŸ¨β€œπ‘β€βŸ© ∈ dom 𝑆)
9995, 98sylbir 234 . . . . . . . . . . . . . . . . . 18 ((𝑐 ∈ π‘Š ∧ Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)) β†’ βŸ¨β€œπ‘β€βŸ© ∈ dom 𝑆)
1001, 2, 3, 4, 5, 6efgsval 19520 . . . . . . . . . . . . . . . . . 18 (βŸ¨β€œπ‘β€βŸ© ∈ dom 𝑆 β†’ (π‘†β€˜βŸ¨β€œπ‘β€βŸ©) = (βŸ¨β€œπ‘β€βŸ©β€˜((β™―β€˜βŸ¨β€œπ‘β€βŸ©) βˆ’ 1)))
10199, 100syl 17 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ π‘Š ∧ Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)) β†’ (π‘†β€˜βŸ¨β€œπ‘β€βŸ©) = (βŸ¨β€œπ‘β€βŸ©β€˜((β™―β€˜βŸ¨β€œπ‘β€βŸ©) βˆ’ 1)))
102 s1len 14501 . . . . . . . . . . . . . . . . . . . . 21 (β™―β€˜βŸ¨β€œπ‘β€βŸ©) = 1
103102oveq1i 7372 . . . . . . . . . . . . . . . . . . . 20 ((β™―β€˜βŸ¨β€œπ‘β€βŸ©) βˆ’ 1) = (1 βˆ’ 1)
104 1m1e0 12232 . . . . . . . . . . . . . . . . . . . 20 (1 βˆ’ 1) = 0
105103, 104eqtri 2765 . . . . . . . . . . . . . . . . . . 19 ((β™―β€˜βŸ¨β€œπ‘β€βŸ©) βˆ’ 1) = 0
106105fveq2i 6850 . . . . . . . . . . . . . . . . . 18 (βŸ¨β€œπ‘β€βŸ©β€˜((β™―β€˜βŸ¨β€œπ‘β€βŸ©) βˆ’ 1)) = (βŸ¨β€œπ‘β€βŸ©β€˜0)
107106a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ π‘Š ∧ Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)) β†’ (βŸ¨β€œπ‘β€βŸ©β€˜((β™―β€˜βŸ¨β€œπ‘β€βŸ©) βˆ’ 1)) = (βŸ¨β€œπ‘β€βŸ©β€˜0))
108 s1fv 14505 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ π‘Š β†’ (βŸ¨β€œπ‘β€βŸ©β€˜0) = 𝑐)
109108adantr 482 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ π‘Š ∧ Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)) β†’ (βŸ¨β€œπ‘β€βŸ©β€˜0) = 𝑐)
110101, 107, 1093eqtrd 2781 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ π‘Š ∧ Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)) β†’ (π‘†β€˜βŸ¨β€œπ‘β€βŸ©) = 𝑐)
111 fnfvelrn 7036 . . . . . . . . . . . . . . . . 17 ((𝑆 Fn dom 𝑆 ∧ βŸ¨β€œπ‘β€βŸ© ∈ dom 𝑆) β†’ (π‘†β€˜βŸ¨β€œπ‘β€βŸ©) ∈ ran 𝑆)
11269, 99, 111sylancr 588 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ π‘Š ∧ Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)) β†’ (π‘†β€˜βŸ¨β€œπ‘β€βŸ©) ∈ ran 𝑆)
113110, 112eqeltrrd 2839 . . . . . . . . . . . . . . 15 ((𝑐 ∈ π‘Š ∧ Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯)) β†’ 𝑐 ∈ ran 𝑆)
114113ex 414 . . . . . . . . . . . . . 14 (𝑐 ∈ π‘Š β†’ (Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯) β†’ 𝑐 ∈ ran 𝑆))
1151143ad2ant2 1135 . . . . . . . . . . . . 13 (((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) β†’ (Β¬ 𝑐 ∈ βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯) β†’ 𝑐 ∈ ran 𝑆))
11694, 115pm2.61d 179 . . . . . . . . . . . 12 (((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) ∧ 𝑐 ∈ π‘Š ∧ (β™―β€˜π‘) = 𝑑) β†’ 𝑐 ∈ ran 𝑆)
117116rabssdv 4037 . . . . . . . . . . 11 ((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) β†’ {𝑐 ∈ π‘Š ∣ (β™―β€˜π‘) = 𝑑} βŠ† ran 𝑆)
11843, 117eqsstrid 3997 . . . . . . . . . 10 ((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) = 𝑑} βŠ† ran 𝑆)
11941, 118unssd 4151 . . . . . . . . 9 ((𝑑 ∈ β„•0 ∧ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆) β†’ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βˆͺ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) = 𝑑}) βŠ† ran 𝑆)
120119ex 414 . . . . . . . 8 (𝑑 ∈ β„•0 β†’ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆 β†’ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βˆͺ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) = 𝑑}) βŠ† ran 𝑆))
121 id 22 . . . . . . . . . . . . 13 (𝑑 ∈ β„•0 β†’ 𝑑 ∈ β„•0)
122 nn0leltp1 12569 . . . . . . . . . . . . 13 (((β™―β€˜π‘Ž) ∈ β„•0 ∧ 𝑑 ∈ β„•0) β†’ ((β™―β€˜π‘Ž) ≀ 𝑑 ↔ (β™―β€˜π‘Ž) < (𝑑 + 1)))
12321, 121, 122syl2anr 598 . . . . . . . . . . . 12 ((𝑑 ∈ β„•0 ∧ π‘Ž ∈ π‘Š) β†’ ((β™―β€˜π‘Ž) ≀ 𝑑 ↔ (β™―β€˜π‘Ž) < (𝑑 + 1)))
12421nn0red 12481 . . . . . . . . . . . . 13 (π‘Ž ∈ π‘Š β†’ (β™―β€˜π‘Ž) ∈ ℝ)
125 nn0re 12429 . . . . . . . . . . . . 13 (𝑑 ∈ β„•0 β†’ 𝑑 ∈ ℝ)
126 leloe 11248 . . . . . . . . . . . . 13 (((β™―β€˜π‘Ž) ∈ ℝ ∧ 𝑑 ∈ ℝ) β†’ ((β™―β€˜π‘Ž) ≀ 𝑑 ↔ ((β™―β€˜π‘Ž) < 𝑑 ∨ (β™―β€˜π‘Ž) = 𝑑)))
127124, 125, 126syl2anr 598 . . . . . . . . . . . 12 ((𝑑 ∈ β„•0 ∧ π‘Ž ∈ π‘Š) β†’ ((β™―β€˜π‘Ž) ≀ 𝑑 ↔ ((β™―β€˜π‘Ž) < 𝑑 ∨ (β™―β€˜π‘Ž) = 𝑑)))
128123, 127bitr3d 281 . . . . . . . . . . 11 ((𝑑 ∈ β„•0 ∧ π‘Ž ∈ π‘Š) β†’ ((β™―β€˜π‘Ž) < (𝑑 + 1) ↔ ((β™―β€˜π‘Ž) < 𝑑 ∨ (β™―β€˜π‘Ž) = 𝑑)))
129128rabbidva 3417 . . . . . . . . . 10 (𝑑 ∈ β„•0 β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < (𝑑 + 1)} = {π‘Ž ∈ π‘Š ∣ ((β™―β€˜π‘Ž) < 𝑑 ∨ (β™―β€˜π‘Ž) = 𝑑)})
130 unrab 4270 . . . . . . . . . 10 ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βˆͺ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) = 𝑑}) = {π‘Ž ∈ π‘Š ∣ ((β™―β€˜π‘Ž) < 𝑑 ∨ (β™―β€˜π‘Ž) = 𝑑)}
131129, 130eqtr4di 2795 . . . . . . . . 9 (𝑑 ∈ β„•0 β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < (𝑑 + 1)} = ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βˆͺ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) = 𝑑}))
132131sseq1d 3980 . . . . . . . 8 (𝑑 ∈ β„•0 β†’ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < (𝑑 + 1)} βŠ† ran 𝑆 ↔ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βˆͺ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) = 𝑑}) βŠ† ran 𝑆))
133120, 132sylibrd 259 . . . . . . 7 (𝑑 ∈ β„•0 β†’ ({π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < 𝑑} βŠ† ran 𝑆 β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < (𝑑 + 1)} βŠ† ran 𝑆))
13430, 33, 36, 39, 40, 133nn0ind 12605 . . . . . 6 (((β™―β€˜π‘) + 1) ∈ β„•0 β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < ((β™―β€˜π‘) + 1)} βŠ† ran 𝑆)
13517, 18, 1343syl 18 . . . . 5 (𝑐 ∈ π‘Š β†’ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < ((β™―β€˜π‘) + 1)} βŠ† ran 𝑆)
136 fveq2 6847 . . . . . . 7 (π‘Ž = 𝑐 β†’ (β™―β€˜π‘Ž) = (β™―β€˜π‘))
137136breq1d 5120 . . . . . 6 (π‘Ž = 𝑐 β†’ ((β™―β€˜π‘Ž) < ((β™―β€˜π‘) + 1) ↔ (β™―β€˜π‘) < ((β™―β€˜π‘) + 1)))
138 id 22 . . . . . 6 (𝑐 ∈ π‘Š β†’ 𝑐 ∈ π‘Š)
13917nn0red 12481 . . . . . . 7 (𝑐 ∈ π‘Š β†’ (β™―β€˜π‘) ∈ ℝ)
140139ltp1d 12092 . . . . . 6 (𝑐 ∈ π‘Š β†’ (β™―β€˜π‘) < ((β™―β€˜π‘) + 1))
141137, 138, 140elrabd 3652 . . . . 5 (𝑐 ∈ π‘Š β†’ 𝑐 ∈ {π‘Ž ∈ π‘Š ∣ (β™―β€˜π‘Ž) < ((β™―β€˜π‘) + 1)})
142135, 141sseldd 3950 . . . 4 (𝑐 ∈ π‘Š β†’ 𝑐 ∈ ran 𝑆)
143142ssriv 3953 . . 3 π‘Š βŠ† ran 𝑆
14412, 143eqssi 3965 . 2 ran 𝑆 = π‘Š
145 dffo2 6765 . 2 (𝑆:dom 𝑆–ontoβ†’π‘Š ↔ (𝑆:dom π‘†βŸΆπ‘Š ∧ ran 𝑆 = π‘Š))
14610, 144, 145mpbir2an 710 1 𝑆:dom 𝑆–ontoβ†’π‘Š
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3065  βˆƒwrex 3074  {crab 3410   βˆ– cdif 3912   βˆͺ cun 3913   βŠ† wss 3915  βˆ…c0 4287  {csn 4591  βŸ¨cop 4597  βŸ¨cotp 4599  βˆͺ ciun 4959   class class class wbr 5110   ↦ cmpt 5193   I cid 5535   Γ— cxp 5636  dom cdm 5638  ran crn 5639   Fn wfn 6496  βŸΆwf 6497  β€“ontoβ†’wfo 6499  β€˜cfv 6501  (class class class)co 7362   ∈ cmpo 7364  1oc1o 8410  2oc2o 8411  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  2c2 12215  β„•0cn0 12420  β„+crp 12922  ...cfz 13431  ..^cfzo 13574  β™―chash 14237  Word cword 14409   ++ cconcat 14465  βŸ¨β€œcs1 14490   splice csplice 14644  βŸ¨β€œcs2 14737   ~FG cefg 19495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-ot 4600  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-rp 12923  df-fz 13432  df-fzo 13575  df-hash 14238  df-word 14410  df-concat 14466  df-s1 14491  df-substr 14536  df-pfx 14566  df-splice 14645  df-s2 14744
This theorem is referenced by:  efgredlemc  19534  efgrelexlemb  19539  efgredeu  19541  efgred2  19542
  Copyright terms: Public domain W3C validator