This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ccatf1

Description: Conditions for a concatenation to be injective. (Contributed by Thierry Arnoux, 11-Dec-2023)

Ref Expression
Hypotheses ccatf1.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
ccatf1.a ⊢ ( 𝜑 → 𝐴 ∈ Word 𝑆 )
ccatf1.b ⊢ ( 𝜑 → 𝐵 ∈ Word 𝑆 )
ccatf1.1 ⊢ ( 𝜑 → 𝐴 : dom 𝐴 –1-1→ 𝑆 )
ccatf1.2 ⊢ ( 𝜑 → 𝐵 : dom 𝐵 –1-1→ 𝑆 )
ccatf1.3 ⊢ ( 𝜑 → ( ran 𝐴 ∩ ran 𝐵 ) = ∅ )
Assertion ccatf1 ( 𝜑 → ( 𝐴 ++ 𝐵 ) : dom ( 𝐴 ++ 𝐵 ) –1-1→ 𝑆 )

Proof

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