| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ccatvalfn 14620 | . . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) Fn (0..^((♯‘𝑆) + (♯‘𝑇)))) | 
| 2 |  | lencl 14572 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
ℕ0) | 
| 3 |  | nn0uz 12921 | . . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) | 
| 4 | 2, 3 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
(ℤ≥‘0)) | 
| 5 | 4 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈
(ℤ≥‘0)) | 
| 6 | 2 | nn0zd 12641 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈ ℤ) | 
| 7 | 6 | uzidd 12895 | . . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
(ℤ≥‘(♯‘𝑆))) | 
| 8 |  | lencl 14572 | . . . . . . . . . . 11
⊢ (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈
ℕ0) | 
| 9 |  | uzaddcl 12947 | . . . . . . . . . . 11
⊢
(((♯‘𝑆)
∈ (ℤ≥‘(♯‘𝑆)) ∧ (♯‘𝑇) ∈ ℕ0) →
((♯‘𝑆) +
(♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆))) | 
| 10 | 7, 8, 9 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆))) | 
| 11 |  | elfzuzb 13559 | . . . . . . . . . 10
⊢
((♯‘𝑆)
∈ (0...((♯‘𝑆) + (♯‘𝑇))) ↔ ((♯‘𝑆) ∈ (ℤ≥‘0)
∧ ((♯‘𝑆) +
(♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆)))) | 
| 12 | 5, 10, 11 | sylanbrc 583 | . . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈ (0...((♯‘𝑆) + (♯‘𝑇)))) | 
| 13 |  | fzosplit 13733 | . . . . . . . . 9
⊢
((♯‘𝑆)
∈ (0...((♯‘𝑆) + (♯‘𝑇))) → (0..^((♯‘𝑆) + (♯‘𝑇))) = ((0..^(♯‘𝑆)) ∪ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) | 
| 14 | 12, 13 | syl 17 | . . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^((♯‘𝑆) + (♯‘𝑇))) = ((0..^(♯‘𝑆)) ∪ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) | 
| 15 | 14 | eleq2d 2826 | . . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↔ 𝑥 ∈ ((0..^(♯‘𝑆)) ∪ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))))) | 
| 16 |  | elun 4152 | . . . . . . 7
⊢ (𝑥 ∈
((0..^(♯‘𝑆))
∪ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) ↔ (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) | 
| 17 | 15, 16 | bitrdi 287 | . . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↔ (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))))) | 
| 18 |  | ccatval1 14616 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆‘𝑥)) | 
| 19 | 18 | 3expa 1118 | . . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆‘𝑥)) | 
| 20 |  | ssun1 4177 | . . . . . . . . . 10
⊢ ran 𝑆 ⊆ (ran 𝑆 ∪ ran 𝑇) | 
| 21 |  | wrdfn 14567 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → 𝑆 Fn (0..^(♯‘𝑆))) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆 Fn (0..^(♯‘𝑆))) | 
| 23 |  | fnfvelrn 7099 | . . . . . . . . . . 11
⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ ran 𝑆) | 
| 24 | 22, 23 | sylan 580 | . . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ ran 𝑆) | 
| 25 | 20, 24 | sselid 3980 | . . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) | 
| 26 | 19, 25 | eqeltrd 2840 | . . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) | 
| 27 |  | ccatval2 14617 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (♯‘𝑆)))) | 
| 28 | 27 | 3expa 1118 | . . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (♯‘𝑆)))) | 
| 29 |  | ssun2 4178 | . . . . . . . . . 10
⊢ ran 𝑇 ⊆ (ran 𝑆 ∪ ran 𝑇) | 
| 30 |  | wrdfn 14567 | . . . . . . . . . . . 12
⊢ (𝑇 ∈ Word 𝐵 → 𝑇 Fn (0..^(♯‘𝑇))) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇 Fn (0..^(♯‘𝑇))) | 
| 32 |  | elfzouz 13704 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → 𝑥 ∈
(ℤ≥‘(♯‘𝑆))) | 
| 33 |  | uznn0sub 12918 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
(ℤ≥‘(♯‘𝑆)) → (𝑥 − (♯‘𝑆)) ∈
ℕ0) | 
| 34 | 32, 33 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → (𝑥 − (♯‘𝑆)) ∈
ℕ0) | 
| 35 | 34, 3 | eleqtrdi 2850 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → (𝑥 − (♯‘𝑆)) ∈
(ℤ≥‘0)) | 
| 36 | 35 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 − (♯‘𝑆)) ∈
(ℤ≥‘0)) | 
| 37 | 8 | nn0zd 12641 | . . . . . . . . . . . . 13
⊢ (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈ ℤ) | 
| 38 | 37 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (♯‘𝑇) ∈ ℤ) | 
| 39 |  | elfzolt2 13709 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → 𝑥 < ((♯‘𝑆) + (♯‘𝑇))) | 
| 40 | 39 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑥 < ((♯‘𝑆) + (♯‘𝑇))) | 
| 41 |  | elfzoelz 13700 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → 𝑥 ∈ ℤ) | 
| 42 | 41 | zred 12724 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → 𝑥 ∈ ℝ) | 
| 43 | 42 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑥 ∈ ℝ) | 
| 44 | 2 | nn0red 12590 | . . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈ ℝ) | 
| 45 | 44 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (♯‘𝑆) ∈ ℝ) | 
| 46 | 8 | nn0red 12590 | . . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈ ℝ) | 
| 47 | 46 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (♯‘𝑇) ∈ ℝ) | 
| 48 | 43, 45, 47 | ltsubadd2d 11862 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑥 − (♯‘𝑆)) < (♯‘𝑇) ↔ 𝑥 < ((♯‘𝑆) + (♯‘𝑇)))) | 
| 49 | 40, 48 | mpbird 257 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 − (♯‘𝑆)) < (♯‘𝑇)) | 
| 50 |  | elfzo2 13703 | . . . . . . . . . . . 12
⊢ ((𝑥 − (♯‘𝑆)) ∈
(0..^(♯‘𝑇))
↔ ((𝑥 −
(♯‘𝑆)) ∈
(ℤ≥‘0) ∧ (♯‘𝑇) ∈ ℤ ∧ (𝑥 − (♯‘𝑆)) < (♯‘𝑇))) | 
| 51 | 36, 38, 49, 50 | syl3anbrc 1343 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇))) | 
| 52 |  | fnfvelrn 7099 | . . . . . . . . . . 11
⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇))) → (𝑇‘(𝑥 − (♯‘𝑆))) ∈ ran 𝑇) | 
| 53 | 31, 51, 52 | syl2an2r 685 | . . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑇‘(𝑥 − (♯‘𝑆))) ∈ ran 𝑇) | 
| 54 | 29, 53 | sselid 3980 | . . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑇‘(𝑥 − (♯‘𝑆))) ∈ (ran 𝑆 ∪ ran 𝑇)) | 
| 55 | 28, 54 | eqeltrd 2840 | . . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) | 
| 56 | 26, 55 | jaodan 959 | . . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) | 
| 57 | 56 | ex 412 | . . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇))) | 
| 58 | 17, 57 | sylbid 240 | . . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇))) | 
| 59 | 58 | ralrimiv 3144 | . . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ∀𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) | 
| 60 |  | ffnfv 7138 | . . . 4
⊢ ((𝑆 ++ 𝑇):(0..^((♯‘𝑆) + (♯‘𝑇)))⟶(ran 𝑆 ∪ ran 𝑇) ↔ ((𝑆 ++ 𝑇) Fn (0..^((♯‘𝑆) + (♯‘𝑇))) ∧ ∀𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇))) | 
| 61 | 1, 59, 60 | sylanbrc 583 | . . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇):(0..^((♯‘𝑆) + (♯‘𝑇)))⟶(ran 𝑆 ∪ ran 𝑇)) | 
| 62 | 61 | frnd 6743 | . 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) ⊆ (ran 𝑆 ∪ ran 𝑇)) | 
| 63 |  | fzoss2 13728 | . . . . . . . . . 10
⊢
(((♯‘𝑆)
+ (♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆)) → (0..^(♯‘𝑆)) ⊆
(0..^((♯‘𝑆) +
(♯‘𝑇)))) | 
| 64 | 10, 63 | syl 17 | . . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^(♯‘𝑆)) ⊆
(0..^((♯‘𝑆) +
(♯‘𝑇)))) | 
| 65 | 64 | sselda 3982 | . . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) | 
| 66 |  | fnfvelrn 7099 | . . . . . . . 8
⊢ (((𝑆 ++ 𝑇) Fn (0..^((♯‘𝑆) + (♯‘𝑇))) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ ran (𝑆 ++ 𝑇)) | 
| 67 | 1, 65, 66 | syl2an2r 685 | . . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ ran (𝑆 ++ 𝑇)) | 
| 68 | 19, 67 | eqeltrrd 2841 | . . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ ran (𝑆 ++ 𝑇)) | 
| 69 | 68 | ralrimiva 3145 | . . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ∀𝑥 ∈ (0..^(♯‘𝑆))(𝑆‘𝑥) ∈ ran (𝑆 ++ 𝑇)) | 
| 70 |  | ffnfv 7138 | . . . . 5
⊢ (𝑆:(0..^(♯‘𝑆))⟶ran (𝑆 ++ 𝑇) ↔ (𝑆 Fn (0..^(♯‘𝑆)) ∧ ∀𝑥 ∈ (0..^(♯‘𝑆))(𝑆‘𝑥) ∈ ran (𝑆 ++ 𝑇))) | 
| 71 | 22, 69, 70 | sylanbrc 583 | . . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆:(0..^(♯‘𝑆))⟶ran (𝑆 ++ 𝑇)) | 
| 72 | 71 | frnd 6743 | . . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran 𝑆 ⊆ ran (𝑆 ++ 𝑇)) | 
| 73 |  | ccatval3 14618 | . . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑥 + (♯‘𝑆))) = (𝑇‘𝑥)) | 
| 74 | 73 | 3expa 1118 | . . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑥 + (♯‘𝑆))) = (𝑇‘𝑥)) | 
| 75 |  | elfzouz 13704 | . . . . . . . . . 10
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
(ℤ≥‘0)) | 
| 76 | 2 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈
ℕ0) | 
| 77 |  | uzaddcl 12947 | . . . . . . . . . 10
⊢ ((𝑥 ∈
(ℤ≥‘0) ∧ (♯‘𝑆) ∈ ℕ0) → (𝑥 + (♯‘𝑆)) ∈
(ℤ≥‘0)) | 
| 78 | 75, 76, 77 | syl2anr 597 | . . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 + (♯‘𝑆)) ∈
(ℤ≥‘0)) | 
| 79 |  | nn0addcl 12563 | . . . . . . . . . . . 12
⊢
(((♯‘𝑆)
∈ ℕ0 ∧ (♯‘𝑇) ∈ ℕ0) →
((♯‘𝑆) +
(♯‘𝑇)) ∈
ℕ0) | 
| 80 | 2, 8, 79 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈
ℕ0) | 
| 81 | 80 | nn0zd 12641 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ) | 
| 82 | 81 | adantr 480 | . . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ) | 
| 83 |  | elfzonn0 13748 | . . . . . . . . . . . 12
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℕ0) | 
| 84 | 83 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℂ) | 
| 85 | 2 | nn0cnd 12591 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈ ℂ) | 
| 86 | 85 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈ ℂ) | 
| 87 |  | addcom 11448 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(♯‘𝑆) ∈
ℂ) → (𝑥 +
(♯‘𝑆)) =
((♯‘𝑆) + 𝑥)) | 
| 88 | 84, 86, 87 | syl2anr 597 | . . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 + (♯‘𝑆)) = ((♯‘𝑆) + 𝑥)) | 
| 89 | 83 | nn0red 12590 | . . . . . . . . . . . 12
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℝ) | 
| 90 | 89 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℝ) | 
| 91 | 46 | ad2antlr 727 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (♯‘𝑇) ∈ ℝ) | 
| 92 | 44 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (♯‘𝑆) ∈ ℝ) | 
| 93 |  | elfzolt2 13709 | . . . . . . . . . . . 12
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 <
(♯‘𝑇)) | 
| 94 | 93 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 < (♯‘𝑇)) | 
| 95 | 90, 91, 92, 94 | ltadd2dd 11421 | . . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((♯‘𝑆) + 𝑥) < ((♯‘𝑆) + (♯‘𝑇))) | 
| 96 | 88, 95 | eqbrtrd 5164 | . . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 + (♯‘𝑆)) < ((♯‘𝑆) + (♯‘𝑇))) | 
| 97 |  | elfzo2 13703 | . . . . . . . . 9
⊢ ((𝑥 + (♯‘𝑆)) ∈
(0..^((♯‘𝑆) +
(♯‘𝑇))) ↔
((𝑥 + (♯‘𝑆)) ∈
(ℤ≥‘0) ∧ ((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ ∧ (𝑥 + (♯‘𝑆)) < ((♯‘𝑆) + (♯‘𝑇)))) | 
| 98 | 78, 82, 96, 97 | syl3anbrc 1343 | . . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 + (♯‘𝑆)) ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) | 
| 99 |  | fnfvelrn 7099 | . . . . . . . 8
⊢ (((𝑆 ++ 𝑇) Fn (0..^((♯‘𝑆) + (♯‘𝑇))) ∧ (𝑥 + (♯‘𝑆)) ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘(𝑥 + (♯‘𝑆))) ∈ ran (𝑆 ++ 𝑇)) | 
| 100 | 1, 98, 99 | syl2an2r 685 | . . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑥 + (♯‘𝑆))) ∈ ran (𝑆 ++ 𝑇)) | 
| 101 | 74, 100 | eqeltrrd 2841 | . . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ ran (𝑆 ++ 𝑇)) | 
| 102 | 101 | ralrimiva 3145 | . . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ∀𝑥 ∈ (0..^(♯‘𝑇))(𝑇‘𝑥) ∈ ran (𝑆 ++ 𝑇)) | 
| 103 |  | ffnfv 7138 | . . . . 5
⊢ (𝑇:(0..^(♯‘𝑇))⟶ran (𝑆 ++ 𝑇) ↔ (𝑇 Fn (0..^(♯‘𝑇)) ∧ ∀𝑥 ∈ (0..^(♯‘𝑇))(𝑇‘𝑥) ∈ ran (𝑆 ++ 𝑇))) | 
| 104 | 31, 102, 103 | sylanbrc 583 | . . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇:(0..^(♯‘𝑇))⟶ran (𝑆 ++ 𝑇)) | 
| 105 | 104 | frnd 6743 | . . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran 𝑇 ⊆ ran (𝑆 ++ 𝑇)) | 
| 106 | 72, 105 | unssd 4191 | . 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (ran 𝑆 ∪ ran 𝑇) ⊆ ran (𝑆 ++ 𝑇)) | 
| 107 | 62, 106 | eqssd 4000 | 1
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇)) |