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

Theorem efgredlem 18425
Description: The reduced word that forms the base of the sequence in efgsval 18408 is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015.) (Proof shortened by AV, 3-Nov-2022.)
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)))
efgredlem.1 (𝜑 → ∀𝑎 ∈ dom 𝑆𝑏 ∈ dom 𝑆((♯‘(𝑆𝑎)) < (♯‘(𝑆𝐴)) → ((𝑆𝑎) = (𝑆𝑏) → (𝑎‘0) = (𝑏‘0))))
efgredlem.2 (𝜑𝐴 ∈ dom 𝑆)
efgredlem.3 (𝜑𝐵 ∈ dom 𝑆)
efgredlem.4 (𝜑 → (𝑆𝐴) = (𝑆𝐵))
efgredlem.5 (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))
Assertion
Ref Expression
efgredlem ¬ 𝜑
Distinct variable groups:   𝑎,𝑏,𝐴   𝑦,𝑎,𝑧,𝑏   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧   𝑚,𝑎,𝑛,𝑡,𝑣,𝑤,𝑥,𝑀,𝑏   𝑘,𝑎,𝑇,𝑏,𝑚,𝑡,𝑥   𝑊,𝑎,𝑏   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ,𝑎,𝑏,𝑚,𝑡,𝑥,𝑦,𝑧   𝐵,𝑎,𝑏   𝑆,𝑎,𝑏   𝐼,𝑎,𝑏,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑎,𝑏,𝑚,𝑡
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛,𝑎,𝑏)   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐼(𝑘)   𝑀(𝑦,𝑧,𝑘)

Proof of Theorem efgredlem
Dummy variables 𝑖 𝑗 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . . . . . . . . 10 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
2 fviss 6445 . . . . . . . . . 10 ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
31, 2eqsstri 3795 . . . . . . . . 9 𝑊 ⊆ Word (𝐼 × 2𝑜)
4 efgredlem.2 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ dom 𝑆)
5 efgval.r . . . . . . . . . . . . . . 15 = ( ~FG𝐼)
6 efgval2.m . . . . . . . . . . . . . . 15 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
7 efgval2.t . . . . . . . . . . . . . . 15 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
8 efgred.d . . . . . . . . . . . . . . 15 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
9 efgred.s . . . . . . . . . . . . . . 15 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
101, 5, 6, 7, 8, 9efgsdm 18407 . . . . . . . . . . . . . 14 (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐴))(𝐴𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1)))))
1110simp1bi 1175 . . . . . . . . . . . . 13 (𝐴 ∈ dom 𝑆𝐴 ∈ (Word 𝑊 ∖ {∅}))
124, 11syl 17 . . . . . . . . . . . 12 (𝜑𝐴 ∈ (Word 𝑊 ∖ {∅}))
1312eldifad 3744 . . . . . . . . . . 11 (𝜑𝐴 ∈ Word 𝑊)
14 wrdf 13491 . . . . . . . . . . 11 (𝐴 ∈ Word 𝑊𝐴:(0..^(♯‘𝐴))⟶𝑊)
1513, 14syl 17 . . . . . . . . . 10 (𝜑𝐴:(0..^(♯‘𝐴))⟶𝑊)
16 efgredlem.1 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑎 ∈ dom 𝑆𝑏 ∈ dom 𝑆((♯‘(𝑆𝑎)) < (♯‘(𝑆𝐴)) → ((𝑆𝑎) = (𝑆𝑏) → (𝑎‘0) = (𝑏‘0))))
17 efgredlem.3 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ dom 𝑆)
18 efgredlem.4 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆𝐴) = (𝑆𝐵))
19 efgredlem.5 . . . . . . . . . . . . . . 15 (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))
201, 5, 6, 7, 8, 9, 16, 4, 17, 18, 19efgredlema 18418 . . . . . . . . . . . . . 14 (𝜑 → (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ∈ ℕ))
2120simpld 488 . . . . . . . . . . . . 13 (𝜑 → ((♯‘𝐴) − 1) ∈ ℕ)
22 nnm1nn0 11581 . . . . . . . . . . . . 13 (((♯‘𝐴) − 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
2321, 22syl 17 . . . . . . . . . . . 12 (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ ℕ0)
2421nnred 11291 . . . . . . . . . . . . 13 (𝜑 → ((♯‘𝐴) − 1) ∈ ℝ)
2524lem1d 11211 . . . . . . . . . . . 12 (𝜑 → (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))
26 eldifsni 4476 . . . . . . . . . . . . . . 15 (𝐴 ∈ (Word 𝑊 ∖ {∅}) → 𝐴 ≠ ∅)
274, 11, 263syl 18 . . . . . . . . . . . . . 14 (𝜑𝐴 ≠ ∅)
28 wrdfin 13504 . . . . . . . . . . . . . . 15 (𝐴 ∈ Word 𝑊𝐴 ∈ Fin)
29 hashnncl 13359 . . . . . . . . . . . . . . 15 (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3013, 28, 293syl 18 . . . . . . . . . . . . . 14 (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3127, 30mpbird 248 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐴) ∈ ℕ)
32 nnm1nn0 11581 . . . . . . . . . . . . 13 ((♯‘𝐴) ∈ ℕ → ((♯‘𝐴) − 1) ∈ ℕ0)
33 fznn0 12639 . . . . . . . . . . . . 13 (((♯‘𝐴) − 1) ∈ ℕ0 → ((((♯‘𝐴) − 1) − 1) ∈ (0...((♯‘𝐴) − 1)) ↔ ((((♯‘𝐴) − 1) − 1) ∈ ℕ0 ∧ (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))))
3431, 32, 333syl 18 . . . . . . . . . . . 12 (𝜑 → ((((♯‘𝐴) − 1) − 1) ∈ (0...((♯‘𝐴) − 1)) ↔ ((((♯‘𝐴) − 1) − 1) ∈ ℕ0 ∧ (((♯‘𝐴) − 1) − 1) ≤ ((♯‘𝐴) − 1))))
3523, 25, 34mpbir2and 704 . . . . . . . . . . 11 (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ (0...((♯‘𝐴) − 1)))
36 lencl 13505 . . . . . . . . . . . . . 14 (𝐴 ∈ Word 𝑊 → (♯‘𝐴) ∈ ℕ0)
3713, 36syl 17 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐴) ∈ ℕ0)
3837nn0zd 11727 . . . . . . . . . . . 12 (𝜑 → (♯‘𝐴) ∈ ℤ)
39 fzoval 12679 . . . . . . . . . . . 12 ((♯‘𝐴) ∈ ℤ → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
4038, 39syl 17 . . . . . . . . . . 11 (𝜑 → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1)))
4135, 40eleqtrrd 2847 . . . . . . . . . 10 (𝜑 → (((♯‘𝐴) − 1) − 1) ∈ (0..^(♯‘𝐴)))
4215, 41ffvelrnd 6550 . . . . . . . . 9 (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊)
433, 42sseldi 3759 . . . . . . . 8 (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2𝑜))
44 lencl 13505 . . . . . . . 8 ((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ Word (𝐼 × 2𝑜) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℕ0)
4543, 44syl 17 . . . . . . 7 (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℕ0)
4645nn0red 11599 . . . . . 6 (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ)
47 2rp 12033 . . . . . 6 2 ∈ ℝ+
48 ltaddrp 12065 . . . . . 6 (((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ∈ ℝ ∧ 2 ∈ ℝ+) → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
4946, 47, 48sylancl 580 . . . . 5 (𝜑 → (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) < ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
5037nn0red 11599 . . . . . . . . . . 11 (𝜑 → (♯‘𝐴) ∈ ℝ)
5150lem1d 11211 . . . . . . . . . 10 (𝜑 → ((♯‘𝐴) − 1) ≤ (♯‘𝐴))
52 fznn 12615 . . . . . . . . . . 11 ((♯‘𝐴) ∈ ℤ → (((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴)) ↔ (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴))))
5338, 52syl 17 . . . . . . . . . 10 (𝜑 → (((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴)) ↔ (((♯‘𝐴) − 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴))))
5421, 51, 53mpbir2and 704 . . . . . . . . 9 (𝜑 → ((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴)))
551, 5, 6, 7, 8, 9efgsres 18415 . . . . . . . . 9 ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ (1...(♯‘𝐴))) → (𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆)
564, 54, 55syl2anc 579 . . . . . . . 8 (𝜑 → (𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆)
571, 5, 6, 7, 8, 9efgsval 18408 . . . . . . . 8 ((𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)))
5856, 57syl 17 . . . . . . 7 (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)))
59 fz1ssfz0 12643 . . . . . . . . . . . 12 (1...(♯‘𝐴)) ⊆ (0...(♯‘𝐴))
6059, 54sseldi 3759 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴)))
61 pfxres 13668 . . . . . . . . . . 11 ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴))) → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1))))
6213, 60, 61syl2anc 579 . . . . . . . . . 10 (𝜑 → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1))))
6362fveq2d 6379 . . . . . . . . 9 (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = (♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))))
64 pfxlen 13672 . . . . . . . . . 10 ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
6513, 60, 64syl2anc 579 . . . . . . . . 9 (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) = ((♯‘𝐴) − 1))
6663, 65eqtr3d 2801 . . . . . . . 8 (𝜑 → (♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((♯‘𝐴) − 1))
6766fvoveq1d 6864 . . . . . . 7 (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)))
68 fzo0end 12768 . . . . . . . 8 (((♯‘𝐴) − 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈ (0..^((♯‘𝐴) − 1)))
69 fvres 6394 . . . . . . . 8 ((((♯‘𝐴) − 1) − 1) ∈ (0..^((♯‘𝐴) − 1)) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
7021, 68, 693syl 18 . . . . . . 7 (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
7158, 67, 703eqtrd 2803 . . . . . 6 (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝐴‘(((♯‘𝐴) − 1) − 1)))
7271fveq2d 6379 . . . . 5 (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) = (♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
731, 5, 6, 7, 8, 9efgsdmi 18409 . . . . . . 7 ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ ℕ) → (𝑆𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
744, 21, 73syl2anc 579 . . . . . 6 (𝜑 → (𝑆𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))))
751, 5, 6, 7efgtlen 18403 . . . . . 6 (((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊 ∧ (𝑆𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) → (♯‘(𝑆𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
7642, 74, 75syl2anc 579 . . . . 5 (𝜑 → (♯‘(𝑆𝐴)) = ((♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))) + 2))
7749, 72, 763brtr4d 4841 . . . 4 (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆𝐴)))
781, 5, 6, 7efgtf 18399 . . . . . . . . . . . 12 ((𝐴‘(((♯‘𝐴) − 1) − 1)) ∈ 𝑊 → ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2𝑜) ↦ ((𝐴‘(((♯‘𝐴) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀𝑏)”⟩⟩)) ∧ (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2𝑜))⟶𝑊))
7942, 78syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2𝑜) ↦ ((𝐴‘(((♯‘𝐴) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀𝑏)”⟩⟩)) ∧ (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2𝑜))⟶𝑊))
8079simprd 489 . . . . . . . . . 10 (𝜑 → (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2𝑜))⟶𝑊)
81 ffn 6223 . . . . . . . . . 10 ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))):((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2𝑜))⟶𝑊 → (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn ((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2𝑜)))
82 ovelrn 7008 . . . . . . . . . 10 ((𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) Fn ((0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) × (𝐼 × 2𝑜)) → ((𝑆𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ↔ ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2𝑜)(𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟)))
8380, 81, 823syl 18 . . . . . . . . 9 (𝜑 → ((𝑆𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) ↔ ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2𝑜)(𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟)))
8474, 83mpbid 223 . . . . . . . 8 (𝜑 → ∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2𝑜)(𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟))
8520simprd 489 . . . . . . . . . 10 (𝜑 → ((♯‘𝐵) − 1) ∈ ℕ)
861, 5, 6, 7, 8, 9efgsdmi 18409 . . . . . . . . . 10 ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ ℕ) → (𝑆𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
8717, 85, 86syl2anc 579 . . . . . . . . 9 (𝜑 → (𝑆𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))))
881, 5, 6, 7, 8, 9efgsdm 18407 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐵))(𝐵𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1)))))
8988simp1bi 1175 . . . . . . . . . . . . . . . 16 (𝐵 ∈ dom 𝑆𝐵 ∈ (Word 𝑊 ∖ {∅}))
9017, 89syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ (Word 𝑊 ∖ {∅}))
9190eldifad 3744 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ Word 𝑊)
92 wrdf 13491 . . . . . . . . . . . . . 14 (𝐵 ∈ Word 𝑊𝐵:(0..^(♯‘𝐵))⟶𝑊)
9391, 92syl 17 . . . . . . . . . . . . 13 (𝜑𝐵:(0..^(♯‘𝐵))⟶𝑊)
94 fzo0end 12768 . . . . . . . . . . . . . . 15 (((♯‘𝐵) − 1) ∈ ℕ → (((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)))
95 elfzofz 12693 . . . . . . . . . . . . . . 15 ((((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)) → (((♯‘𝐵) − 1) − 1) ∈ (0...((♯‘𝐵) − 1)))
9685, 94, 953syl 18 . . . . . . . . . . . . . 14 (𝜑 → (((♯‘𝐵) − 1) − 1) ∈ (0...((♯‘𝐵) − 1)))
97 lencl 13505 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ Word 𝑊 → (♯‘𝐵) ∈ ℕ0)
9891, 97syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘𝐵) ∈ ℕ0)
9998nn0zd 11727 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘𝐵) ∈ ℤ)
100 fzoval 12679 . . . . . . . . . . . . . . 15 ((♯‘𝐵) ∈ ℤ → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
10199, 100syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1)))
10296, 101eleqtrrd 2847 . . . . . . . . . . . . 13 (𝜑 → (((♯‘𝐵) − 1) − 1) ∈ (0..^(♯‘𝐵)))
10393, 102ffvelrnd 6550 . . . . . . . . . . . 12 (𝜑 → (𝐵‘(((♯‘𝐵) − 1) − 1)) ∈ 𝑊)
1041, 5, 6, 7efgtf 18399 . . . . . . . . . . . 12 ((𝐵‘(((♯‘𝐵) − 1) − 1)) ∈ 𝑊 → ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2𝑜) ↦ ((𝐵‘(((♯‘𝐵) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀𝑏)”⟩⟩)) ∧ (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2𝑜))⟶𝑊))
105103, 104syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) = (𝑎 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))), 𝑏 ∈ (𝐼 × 2𝑜) ↦ ((𝐵‘(((♯‘𝐵) − 1) − 1)) splice ⟨𝑎, 𝑎, ⟨“𝑏(𝑀𝑏)”⟩⟩)) ∧ (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2𝑜))⟶𝑊))
106105simprd 489 . . . . . . . . . 10 (𝜑 → (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2𝑜))⟶𝑊)
107 ffn 6223 . . . . . . . . . 10 ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))):((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2𝑜))⟶𝑊 → (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn ((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2𝑜)))
108 ovelrn 7008 . . . . . . . . . 10 ((𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) Fn ((0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) × (𝐼 × 2𝑜)) → ((𝑆𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) ↔ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2𝑜)(𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
109106, 107, 1083syl 18 . . . . . . . . 9 (𝜑 → ((𝑆𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) ↔ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2𝑜)(𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
11087, 109mpbid 223 . . . . . . . 8 (𝜑 → ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2𝑜)(𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))
111 reeanv 3254 . . . . . . . . 9 (∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))(∃𝑟 ∈ (𝐼 × 2𝑜)(𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2𝑜)(𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2𝑜)(𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2𝑜)(𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
112 reeanv 3254 . . . . . . . . . . 11 (∃𝑟 ∈ (𝐼 × 2𝑜)∃𝑠 ∈ (𝐼 × 2𝑜)((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) ↔ (∃𝑟 ∈ (𝐼 × 2𝑜)(𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2𝑜)(𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
11316ad3antrrr 721 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ∀𝑎 ∈ dom 𝑆𝑏 ∈ dom 𝑆((♯‘(𝑆𝑎)) < (♯‘(𝑆𝐴)) → ((𝑆𝑎) = (𝑆𝑏) → (𝑎‘0) = (𝑏‘0))))
1144ad3antrrr 721 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝐴 ∈ dom 𝑆)
11517ad3antrrr 721 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝐵 ∈ dom 𝑆)
11618ad3antrrr 721 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑆𝐴) = (𝑆𝐵))
11719ad3antrrr 721 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ¬ (𝐴‘0) = (𝐵‘0))
118 eqid 2765 . . . . . . . . . . . . . . 15 (((♯‘𝐴) − 1) − 1) = (((♯‘𝐴) − 1) − 1)
119 eqid 2765 . . . . . . . . . . . . . . 15 (((♯‘𝐵) − 1) − 1) = (((♯‘𝐵) − 1) − 1)
120 simpllr 793 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))))
121120simpld 488 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))))
122120simprd 489 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))
123 simplrl 795 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)))
124123simpld 488 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑟 ∈ (𝐼 × 2𝑜))
125123simprd 489 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → 𝑠 ∈ (𝐼 × 2𝑜))
126 simplrr 796 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))
127126simpld 488 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟))
128126simprd 489 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠))
129 simpr 477 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) → ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
1301, 5, 6, 7, 8, 9, 113, 114, 115, 116, 117, 118, 119, 121, 122, 124, 125, 127, 128, 129efgredlemb 18424 . . . . . . . . . . . . . 14 ¬ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
131 iman 390 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))) ↔ ¬ (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) ∧ ¬ (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
132130, 131mpbir 222 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ ((𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜)) ∧ ((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)))) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
133132expr 448 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) ∧ (𝑟 ∈ (𝐼 × 2𝑜) ∧ 𝑠 ∈ (𝐼 × 2𝑜))) → (((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
134133rexlimdvva 3185 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) → (∃𝑟 ∈ (𝐼 × 2𝑜)∃𝑠 ∈ (𝐼 × 2𝑜)((𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ (𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
135112, 134syl5bir 234 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) ∧ 𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1)))))) → ((∃𝑟 ∈ (𝐼 × 2𝑜)(𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2𝑜)(𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
136135rexlimdvva 3185 . . . . . . . . 9 (𝜑 → (∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))(∃𝑟 ∈ (𝐼 × 2𝑜)(𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑠 ∈ (𝐼 × 2𝑜)(𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
137111, 136syl5bir 234 . . . . . . . 8 (𝜑 → ((∃𝑖 ∈ (0...(♯‘(𝐴‘(((♯‘𝐴) − 1) − 1))))∃𝑟 ∈ (𝐼 × 2𝑜)(𝑆𝐴) = (𝑖(𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))𝑟) ∧ ∃𝑗 ∈ (0...(♯‘(𝐵‘(((♯‘𝐵) − 1) − 1))))∃𝑠 ∈ (𝐼 × 2𝑜)(𝑆𝐵) = (𝑗(𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))𝑠)) → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1))))
13884, 110, 137mp2and 690 . . . . . . 7 (𝜑 → (𝐴‘(((♯‘𝐴) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
139 fvres 6394 . . . . . . . 8 ((((♯‘𝐵) − 1) − 1) ∈ (0..^((♯‘𝐵) − 1)) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
14085, 94, 1393syl 18 . . . . . . 7 (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)) = (𝐵‘(((♯‘𝐵) − 1) − 1)))
141138, 70, 1403eqtr4d 2809 . . . . . 6 (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘(((♯‘𝐴) − 1) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
142 fz1ssfz0 12643 . . . . . . . . . . 11 (1...(♯‘𝐵)) ⊆ (0...(♯‘𝐵))
14398nn0red 11599 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐵) ∈ ℝ)
144143lem1d 11211 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐵) − 1) ≤ (♯‘𝐵))
145 fznn 12615 . . . . . . . . . . . . 13 ((♯‘𝐵) ∈ ℤ → (((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵)) ↔ (((♯‘𝐵) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵))))
14699, 145syl 17 . . . . . . . . . . . 12 (𝜑 → (((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵)) ↔ (((♯‘𝐵) − 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵))))
14785, 144, 146mpbir2and 704 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵)))
148142, 147sseldi 3759 . . . . . . . . . 10 (𝜑 → ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵)))
149 pfxres 13668 . . . . . . . . . 10 ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵))) → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1))))
15091, 148, 149syl2anc 579 . . . . . . . . 9 (𝜑 → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1))))
151150fveq2d 6379 . . . . . . . 8 (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = (♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
152 pfxlen 13672 . . . . . . . . 9 ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈ (0...(♯‘𝐵))) → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
15391, 148, 152syl2anc 579 . . . . . . . 8 (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) = ((♯‘𝐵) − 1))
154151, 153eqtr3d 2801 . . . . . . 7 (𝜑 → (♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((♯‘𝐵) − 1))
155154fvoveq1d 6864 . . . . . 6 (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘(((♯‘𝐵) − 1) − 1)))
156141, 67, 1553eqtr4d 2809 . . . . 5 (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
1571, 5, 6, 7, 8, 9efgsres 18415 . . . . . . 7 ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ (1...(♯‘𝐵))) → (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆)
15817, 147, 157syl2anc 579 . . . . . 6 (𝜑 → (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆)
1591, 5, 6, 7, 8, 9efgsval 18408 . . . . . 6 ((𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
160158, 159syl 17 . . . . 5 (𝜑 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)))
161156, 58, 1603eqtr4d 2809 . . . 4 (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
162 fveq2 6375 . . . . . . . . 9 (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑆𝑎) = (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))))
163162fveq2d 6379 . . . . . . . 8 (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (♯‘(𝑆𝑎)) = (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))))
164163breq1d 4819 . . . . . . 7 (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((♯‘(𝑆𝑎)) < (♯‘(𝑆𝐴)) ↔ (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆𝐴))))
165162eqeq1d 2767 . . . . . . . 8 (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑆𝑎) = (𝑆𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆𝑏)))
166 fveq1 6374 . . . . . . . . 9 (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0))
167166eqeq1d 2767 . . . . . . . 8 (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)))
168165, 167imbi12d 335 . . . . . . 7 (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (((𝑆𝑎) = (𝑆𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))))
169164, 168imbi12d 335 . . . . . 6 (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (((♯‘(𝑆𝑎)) < (♯‘(𝑆𝐴)) → ((𝑆𝑎) = (𝑆𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)))))
170 fveq2 6375 . . . . . . . . 9 (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑆𝑏) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))))
171170eqeq2d 2775 . . . . . . . 8 (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))))
172 fveq1 6374 . . . . . . . . 9 (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑏‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))
173172eqeq2d 2775 . . . . . . . 8 (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0)))
174171, 173imbi12d 335 . . . . . . 7 (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))))
175174imbi2d 331 . . . . . 6 (𝑏 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0)))))
176169, 175rspc2va 3475 . . . . 5 ((((𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆 ∧ (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆) ∧ ∀𝑎 ∈ dom 𝑆𝑏 ∈ dom 𝑆((♯‘(𝑆𝑎)) < (♯‘(𝑆𝐴)) → ((𝑆𝑎) = (𝑆𝑏) → (𝑎‘0) = (𝑏‘0)))) → ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))))
17756, 158, 16, 176syl21anc 866 . . . 4 (𝜑 → ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) < (♯‘(𝑆𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))))
17877, 161, 177mp2d 49 . . 3 (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0))
179 lbfzo0 12716 . . . . 5 (0 ∈ (0..^((♯‘𝐴) − 1)) ↔ ((♯‘𝐴) − 1) ∈ ℕ)
18021, 179sylibr 225 . . . 4 (𝜑 → 0 ∈ (0..^((♯‘𝐴) − 1)))
181180fvresd 6395 . . 3 (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝐴‘0))
182 lbfzo0 12716 . . . . 5 (0 ∈ (0..^((♯‘𝐵) − 1)) ↔ ((♯‘𝐵) − 1) ∈ ℕ)
18385, 182sylibr 225 . . . 4 (𝜑 → 0 ∈ (0..^((♯‘𝐵) − 1)))
184183fvresd 6395 . . 3 (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝐵‘0))
185178, 181, 1843eqtr3d 2807 . 2 (𝜑 → (𝐴‘0) = (𝐵‘0))
186185, 19pm2.65i 185 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  cdif 3729  c0 4079  {csn 4334  cop 4340  cotp 4342   ciun 4676   class class class wbr 4809  cmpt 4888   I cid 5184   × cxp 5275  dom cdm 5277  ran crn 5278  cres 5279   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  cmpt2 6844  1𝑜c1o 7757  2𝑜c2o 7758  Fincfn 8160  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   < clt 10328  cle 10329  cmin 10520  cn 11274  2c2 11327  0cn0 11538  cz 11624  +crp 12028  ...cfz 12533  ..^cfzo 12673  chash 13321  Word cword 13486   prefix cpfx 13661   splice csplice 13763  ⟨“cs2 13870   ~FG cefg 18383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-ot 4343  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fz 12534  df-fzo 12674  df-hash 13322  df-word 13487  df-concat 13542  df-s1 13567  df-substr 13617  df-pfx 13662  df-splice 13765  df-s2 13877
This theorem is referenced by:  efgred  18427
  Copyright terms: Public domain W3C validator