Step | Hyp | Ref
| Expression |
1 | | ccatf1.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ Word 𝑆) |
2 | | ccatf1.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ Word 𝑆) |
3 | | ccatcl 14015 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆) → (𝐴 ++ 𝐵) ∈ Word 𝑆) |
4 | 1, 2, 3 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐴 ++ 𝐵) ∈ Word 𝑆) |
5 | | wrdf 13960 |
. . . 4
⊢ ((𝐴 ++ 𝐵) ∈ Word 𝑆 → (𝐴 ++ 𝐵):(0..^(♯‘(𝐴 ++ 𝐵)))⟶𝑆) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → (𝐴 ++ 𝐵):(0..^(♯‘(𝐴 ++ 𝐵)))⟶𝑆) |
7 | 6 | ffdmd 6535 |
. 2
⊢ (𝜑 → (𝐴 ++ 𝐵):dom (𝐴 ++ 𝐵)⟶𝑆) |
8 | | simpllr 776 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) |
9 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈
(0..^(♯‘𝐴))
→ 𝑖 ∈
(0..^(♯‘𝐴))) |
10 | | ccatval1 14019 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴‘𝑖)) |
11 | 1, 2, 9, 10 | syl2an3an 1423 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴‘𝑖)) |
12 | 11 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴‘𝑖)) |
13 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(0..^(♯‘𝐴))
→ 𝑗 ∈
(0..^(♯‘𝐴))) |
14 | | ccatval1 14019 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑗) = (𝐴‘𝑗)) |
15 | 1, 2, 13, 14 | syl2an3an 1423 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑗) = (𝐴‘𝑗)) |
16 | 15 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑗) = (𝐴‘𝑗)) |
17 | 8, 12, 16 | 3eqtr3d 2781 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝑖) = (𝐴‘𝑗)) |
18 | | wrddm 13962 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Word 𝑆 → dom 𝐴 = (0..^(♯‘𝐴))) |
19 | 1, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐴 = (0..^(♯‘𝐴))) |
20 | | ccatf1.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴:dom 𝐴–1-1→𝑆) |
21 | | f1eq2 6570 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝐴 =
(0..^(♯‘𝐴))
→ (𝐴:dom 𝐴–1-1→𝑆 ↔ 𝐴:(0..^(♯‘𝐴))–1-1→𝑆)) |
22 | 21 | biimpa 480 |
. . . . . . . . . . . . . . . 16
⊢ ((dom
𝐴 =
(0..^(♯‘𝐴))
∧ 𝐴:dom 𝐴–1-1→𝑆) → 𝐴:(0..^(♯‘𝐴))–1-1→𝑆) |
23 | 19, 20, 22 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴:(0..^(♯‘𝐴))–1-1→𝑆) |
24 | | dff13 7024 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴:(0..^(♯‘𝐴))–1-1→𝑆 ↔ (𝐴:(0..^(♯‘𝐴))⟶𝑆 ∧ ∀𝑖 ∈ (0..^(♯‘𝐴))∀𝑗 ∈ (0..^(♯‘𝐴))((𝐴‘𝑖) = (𝐴‘𝑗) → 𝑖 = 𝑗))) |
25 | 24 | simprbi 500 |
. . . . . . . . . . . . . . 15
⊢ (𝐴:(0..^(♯‘𝐴))–1-1→𝑆 → ∀𝑖 ∈ (0..^(♯‘𝐴))∀𝑗 ∈ (0..^(♯‘𝐴))((𝐴‘𝑖) = (𝐴‘𝑗) → 𝑖 = 𝑗)) |
26 | 23, 25 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝐴))∀𝑗 ∈ (0..^(♯‘𝐴))((𝐴‘𝑖) = (𝐴‘𝑗) → 𝑖 = 𝑗)) |
27 | 26 | r19.21bi 3121 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → ∀𝑗 ∈ (0..^(♯‘𝐴))((𝐴‘𝑖) = (𝐴‘𝑗) → 𝑖 = 𝑗)) |
28 | 27 | r19.21bi 3121 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴‘𝑖) = (𝐴‘𝑗) → 𝑖 = 𝑗)) |
29 | 28 | adantllr 719 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴‘𝑖) = (𝐴‘𝑗) → 𝑖 = 𝑗)) |
30 | 17, 29 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → 𝑖 = 𝑗) |
31 | 30 | ex 416 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → (𝑗 ∈ (0..^(♯‘𝐴)) → 𝑖 = 𝑗)) |
32 | 31 | adantllr 719 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → (𝑗 ∈ (0..^(♯‘𝐴)) → 𝑖 = 𝑗)) |
33 | | f1fun 6576 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴:dom 𝐴–1-1→𝑆 → Fun 𝐴) |
34 | 20, 33 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun 𝐴) |
35 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → 𝑖 ∈ (0..^(♯‘𝐴))) |
36 | 19 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → dom 𝐴 = (0..^(♯‘𝐴))) |
37 | 35, 36 | eleqtrrd 2836 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → 𝑖 ∈ dom 𝐴) |
38 | | fvelrn 6854 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐴 ∧ 𝑖 ∈ dom 𝐴) → (𝐴‘𝑖) ∈ ran 𝐴) |
39 | 34, 37, 38 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝑖) ∈ ran 𝐴) |
40 | 39 | ad4ant13 751 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝐴‘𝑖) ∈ ran 𝐴) |
41 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) |
42 | 11 | ad4ant13 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐴‘𝑖)) |
43 | 1 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝐴 ∈ Word 𝑆) |
44 | 2 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝐵 ∈ Word 𝑆) |
45 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) |
46 | | ccatlen 14016 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) |
47 | 1, 2, 46 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) |
48 | 47 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) = ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
49 | 48 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) = ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
50 | 45, 49 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝑗 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
51 | | ccatval2 14021 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ∧ 𝑗 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘𝑗) = (𝐵‘(𝑗 − (♯‘𝐴)))) |
52 | 43, 44, 50, 51 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵)‘𝑗) = (𝐵‘(𝑗 − (♯‘𝐴)))) |
53 | 52 | ad4ant14 752 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵)‘𝑗) = (𝐵‘(𝑗 − (♯‘𝐴)))) |
54 | 41, 42, 53 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝐴‘𝑖) = (𝐵‘(𝑗 − (♯‘𝐴)))) |
55 | | ccatf1.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵:dom 𝐵–1-1→𝑆) |
56 | | f1fun 6576 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵:dom 𝐵–1-1→𝑆 → Fun 𝐵) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Fun 𝐵) |
58 | | lencl 13974 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ Word 𝑆 → (♯‘𝐵) ∈
ℕ0) |
59 | 2, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) |
60 | 59 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (♯‘𝐵) ∈
ℤ) |
61 | 60 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (♯‘𝐵) ∈ ℤ) |
62 | | fzosubel3 13189 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ∧ (♯‘𝐵) ∈ ℤ) → (𝑗 − (♯‘𝐴)) ∈
(0..^(♯‘𝐵))) |
63 | 50, 61, 62 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑗 − (♯‘𝐴)) ∈ (0..^(♯‘𝐵))) |
64 | | wrddm 13962 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Word 𝑆 → dom 𝐵 = (0..^(♯‘𝐵))) |
65 | 2, 64 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom 𝐵 = (0..^(♯‘𝐵))) |
66 | 65 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → dom 𝐵 = (0..^(♯‘𝐵))) |
67 | 63, 66 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑗 − (♯‘𝐴)) ∈ dom 𝐵) |
68 | | fvelrn 6854 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐵 ∧ (𝑗 − (♯‘𝐴)) ∈ dom 𝐵) → (𝐵‘(𝑗 − (♯‘𝐴))) ∈ ran 𝐵) |
69 | 57, 67, 68 | syl2an2r 685 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝐵‘(𝑗 − (♯‘𝐴))) ∈ ran 𝐵) |
70 | 69 | ad4ant14 752 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝐵‘(𝑗 − (♯‘𝐴))) ∈ ran 𝐵) |
71 | 54, 70 | eqeltrd 2833 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝐴‘𝑖) ∈ ran 𝐵) |
72 | 40, 71 | elind 4084 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝐴‘𝑖) ∈ (ran 𝐴 ∩ ran 𝐵)) |
73 | | ccatf1.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran 𝐴 ∩ ran 𝐵) = ∅) |
74 | 73 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (ran 𝐴 ∩ ran 𝐵) = ∅) |
75 | 72, 74 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝐴‘𝑖) ∈ ∅) |
76 | | noel 4219 |
. . . . . . . . . . . 12
⊢ ¬
(𝐴‘𝑖) ∈ ∅ |
77 | 76 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ¬ (𝐴‘𝑖) ∈ ∅) |
78 | 75, 77 | pm2.21dd 198 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝑖 = 𝑗) |
79 | 78 | ex 416 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → (𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑖 = 𝑗)) |
80 | 79 | adantllr 719 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → (𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑖 = 𝑗)) |
81 | | wrddm 13962 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ++ 𝐵) ∈ Word 𝑆 → dom (𝐴 ++ 𝐵) = (0..^(♯‘(𝐴 ++ 𝐵)))) |
82 | 4, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (𝐴 ++ 𝐵) = (0..^(♯‘(𝐴 ++ 𝐵)))) |
83 | 82 | eleq2d 2818 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ dom (𝐴 ++ 𝐵) ↔ 𝑗 ∈ (0..^(♯‘(𝐴 ++ 𝐵))))) |
84 | 83 | biimpa 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) → 𝑗 ∈ (0..^(♯‘(𝐴 ++ 𝐵)))) |
85 | | lencl 13974 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Word 𝑆 → (♯‘𝐴) ∈
ℕ0) |
86 | 1, 85 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
87 | 86 | nn0zd 12166 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐴) ∈
ℤ) |
88 | 87 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) → (♯‘𝐴) ∈ ℤ) |
89 | | fzospliti 13160 |
. . . . . . . . . 10
⊢ ((𝑗 ∈
(0..^(♯‘(𝐴 ++
𝐵))) ∧
(♯‘𝐴) ∈
ℤ) → (𝑗 ∈
(0..^(♯‘𝐴))
∨ 𝑗 ∈
((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))))) |
90 | 84, 88, 89 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) → (𝑗 ∈ (0..^(♯‘𝐴)) ∨ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))))) |
91 | 90 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → (𝑗 ∈ (0..^(♯‘𝐴)) ∨ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))))) |
92 | 32, 80, 91 | mpjaod 859 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ (0..^(♯‘𝐴))) → 𝑖 = 𝑗) |
93 | 92 | ex 416 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) → (𝑖 ∈ (0..^(♯‘𝐴)) → 𝑖 = 𝑗)) |
94 | 93 | adantlrl 720 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ dom (𝐴 ++ 𝐵) ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵))) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) → (𝑖 ∈ (0..^(♯‘𝐴)) → 𝑖 = 𝑗)) |
95 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → 𝑗 ∈ (0..^(♯‘𝐴))) |
96 | 19 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → dom 𝐴 = (0..^(♯‘𝐴))) |
97 | 95, 96 | eleqtrrd 2836 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → 𝑗 ∈ dom 𝐴) |
98 | | fvelrn 6854 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐴 ∧ 𝑗 ∈ dom 𝐴) → (𝐴‘𝑗) ∈ ran 𝐴) |
99 | 34, 97, 98 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝑗) ∈ ran 𝐴) |
100 | 99 | ad4ant14 752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝑗) ∈ ran 𝐴) |
101 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) |
102 | 1 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝐴 ∈ Word 𝑆) |
103 | 2 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝐵 ∈ Word 𝑆) |
104 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) |
105 | 48 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) = ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
106 | 104, 105 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
107 | | ccatval2 14021 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ∧ 𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
108 | 102, 103,
106, 107 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
109 | 108 | ad4ant13 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
110 | 15 | ad4ant14 752 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝑗) = (𝐴‘𝑗)) |
111 | 101, 109,
110 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝑗) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
112 | 60 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (♯‘𝐵) ∈ ℤ) |
113 | | fzosubel3 13189 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ∧ (♯‘𝐵) ∈ ℤ) → (𝑖 − (♯‘𝐴)) ∈
(0..^(♯‘𝐵))) |
114 | 106, 112,
113 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑖 − (♯‘𝐴)) ∈ (0..^(♯‘𝐵))) |
115 | 65 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → dom 𝐵 = (0..^(♯‘𝐵))) |
116 | 114, 115 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑖 − (♯‘𝐴)) ∈ dom 𝐵) |
117 | | fvelrn 6854 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐵 ∧ (𝑖 − (♯‘𝐴)) ∈ dom 𝐵) → (𝐵‘(𝑖 − (♯‘𝐴))) ∈ ran 𝐵) |
118 | 57, 116, 117 | syl2an2r 685 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝐵‘(𝑖 − (♯‘𝐴))) ∈ ran 𝐵) |
119 | 118 | ad4ant13 751 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → (𝐵‘(𝑖 − (♯‘𝐴))) ∈ ran 𝐵) |
120 | 111, 119 | eqeltrd 2833 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝑗) ∈ ran 𝐵) |
121 | 100, 120 | elind 4084 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝑗) ∈ (ran 𝐴 ∩ ran 𝐵)) |
122 | 73 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → (ran 𝐴 ∩ ran 𝐵) = ∅) |
123 | 121, 122 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝑗) ∈ ∅) |
124 | | noel 4219 |
. . . . . . . . . . . 12
⊢ ¬
(𝐴‘𝑗) ∈ ∅ |
125 | 124 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → ¬ (𝐴‘𝑗) ∈ ∅) |
126 | 123, 125 | pm2.21dd 198 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ (0..^(♯‘𝐴))) → 𝑖 = 𝑗) |
127 | 126 | ex 416 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑗 ∈ (0..^(♯‘𝐴)) → 𝑖 = 𝑗)) |
128 | 127 | adantllr 719 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑗 ∈ (0..^(♯‘𝐴)) → 𝑖 = 𝑗)) |
129 | | elfzoelz 13129 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑖 ∈ ℤ) |
130 | 129 | zcnd 12169 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑖 ∈ ℂ) |
131 | 130 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝑖 ∈ ℂ) |
132 | | elfzoelz 13129 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑗 ∈ ℤ) |
133 | 132 | zcnd 12169 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑗 ∈ ℂ) |
134 | 133 | adantl 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝑗 ∈ ℂ) |
135 | 86 | nn0cnd 12038 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝐴) ∈
ℂ) |
136 | 135 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (♯‘𝐴) ∈ ℂ) |
137 | 55 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝐵:dom 𝐵–1-1→𝑆) |
138 | 116 | ad4ant13 751 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑖 − (♯‘𝐴)) ∈ dom 𝐵) |
139 | 67 | ad4ant14 752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑗 − (♯‘𝐴)) ∈ dom 𝐵) |
140 | 138, 139 | jca 515 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((𝑖 − (♯‘𝐴)) ∈ dom 𝐵 ∧ (𝑗 − (♯‘𝐴)) ∈ dom 𝐵)) |
141 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) |
142 | 108 | ad4ant13 751 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵)‘𝑖) = (𝐵‘(𝑖 − (♯‘𝐴)))) |
143 | 52 | ad4ant14 752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵)‘𝑗) = (𝐵‘(𝑗 − (♯‘𝐴)))) |
144 | 141, 142,
143 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝐵‘(𝑖 − (♯‘𝐴))) = (𝐵‘(𝑗 − (♯‘𝐴)))) |
145 | | f1veqaeq 7026 |
. . . . . . . . . . . . 13
⊢ ((𝐵:dom 𝐵–1-1→𝑆 ∧ ((𝑖 − (♯‘𝐴)) ∈ dom 𝐵 ∧ (𝑗 − (♯‘𝐴)) ∈ dom 𝐵)) → ((𝐵‘(𝑖 − (♯‘𝐴))) = (𝐵‘(𝑗 − (♯‘𝐴))) → (𝑖 − (♯‘𝐴)) = (𝑗 − (♯‘𝐴)))) |
146 | 145 | imp 410 |
. . . . . . . . . . . 12
⊢ (((𝐵:dom 𝐵–1-1→𝑆 ∧ ((𝑖 − (♯‘𝐴)) ∈ dom 𝐵 ∧ (𝑗 − (♯‘𝐴)) ∈ dom 𝐵)) ∧ (𝐵‘(𝑖 − (♯‘𝐴))) = (𝐵‘(𝑗 − (♯‘𝐴)))) → (𝑖 − (♯‘𝐴)) = (𝑗 − (♯‘𝐴))) |
147 | 137, 140,
144, 146 | syl21anc 837 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑖 − (♯‘𝐴)) = (𝑗 − (♯‘𝐴))) |
148 | 131, 134,
136, 147 | subcan2d 11117 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝑖 = 𝑗) |
149 | 148 | ex 416 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑖 = 𝑗)) |
150 | 149 | adantllr 719 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑖 = 𝑗)) |
151 | 90 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → (𝑗 ∈ (0..^(♯‘𝐴)) ∨ 𝑗 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))))) |
152 | 128, 150,
151 | mpjaod 859 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) ∧ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵)))) → 𝑖 = 𝑗) |
153 | 152 | ex 416 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵)) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) → (𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑖 = 𝑗)) |
154 | 153 | adantlrl 720 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ dom (𝐴 ++ 𝐵) ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵))) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) → (𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))) → 𝑖 = 𝑗)) |
155 | 82 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ dom (𝐴 ++ 𝐵) ↔ 𝑖 ∈ (0..^(♯‘(𝐴 ++ 𝐵))))) |
156 | 155 | biimpa 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (𝐴 ++ 𝐵)) → 𝑖 ∈ (0..^(♯‘(𝐴 ++ 𝐵)))) |
157 | 87 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ dom (𝐴 ++ 𝐵)) → (♯‘𝐴) ∈ ℤ) |
158 | | fzospliti 13160 |
. . . . . . . 8
⊢ ((𝑖 ∈
(0..^(♯‘(𝐴 ++
𝐵))) ∧
(♯‘𝐴) ∈
ℤ) → (𝑖 ∈
(0..^(♯‘𝐴))
∨ 𝑖 ∈
((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))))) |
159 | 156, 157,
158 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ dom (𝐴 ++ 𝐵)) → (𝑖 ∈ (0..^(♯‘𝐴)) ∨ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))))) |
160 | 159 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ dom (𝐴 ++ 𝐵) ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵))) → (𝑖 ∈ (0..^(♯‘𝐴)) ∨ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))))) |
161 | 160 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ dom (𝐴 ++ 𝐵) ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵))) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) → (𝑖 ∈ (0..^(♯‘𝐴)) ∨ 𝑖 ∈ ((♯‘𝐴)..^(♯‘(𝐴 ++ 𝐵))))) |
162 | 94, 154, 161 | mpjaod 859 |
. . . 4
⊢ (((𝜑 ∧ (𝑖 ∈ dom (𝐴 ++ 𝐵) ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵))) ∧ ((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗)) → 𝑖 = 𝑗) |
163 | 162 | ex 416 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ dom (𝐴 ++ 𝐵) ∧ 𝑗 ∈ dom (𝐴 ++ 𝐵))) → (((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗) → 𝑖 = 𝑗)) |
164 | 163 | ralrimivva 3103 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ dom (𝐴 ++ 𝐵)∀𝑗 ∈ dom (𝐴 ++ 𝐵)(((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗) → 𝑖 = 𝑗)) |
165 | | dff13 7024 |
. 2
⊢ ((𝐴 ++ 𝐵):dom (𝐴 ++ 𝐵)–1-1→𝑆 ↔ ((𝐴 ++ 𝐵):dom (𝐴 ++ 𝐵)⟶𝑆 ∧ ∀𝑖 ∈ dom (𝐴 ++ 𝐵)∀𝑗 ∈ dom (𝐴 ++ 𝐵)(((𝐴 ++ 𝐵)‘𝑖) = ((𝐴 ++ 𝐵)‘𝑗) → 𝑖 = 𝑗))) |
166 | 7, 164, 165 | sylanbrc 586 |
1
⊢ (𝜑 → (𝐴 ++ 𝐵):dom (𝐴 ++ 𝐵)–1-1→𝑆) |