Metamath Proof Explorer

Theorem cats1un

Description: Express a word with an extra symbol as the union of the word and the new value. (Contributed by Mario Carneiro, 28-Feb-2016)

Ref Expression
Assertion cats1un ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) = ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 ccatws1cl ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ∈ Word 𝑋 )
2 wrdf ⊢ ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ∈ Word 𝑋 → ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ) ) ⟶ 𝑋 )
3 1 2 syl ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ) ) ⟶ 𝑋 )
4 ccatws1len ⊢ ( 𝐴 ∈ Word 𝑋 → ( ♯ ‘ ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )
5 4 oveq2d ⊢ ( 𝐴 ∈ Word 𝑋 → ( 0 ..^ ( ♯ ‘ ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
6 lencl ⊢ ( 𝐴 ∈ Word 𝑋 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
7 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
8 6 7 eleqtrdi ⊢ ( 𝐴 ∈ Word 𝑋 → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
9 fzosplitsn ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) )
10 8 9 syl ⊢ ( 𝐴 ∈ Word 𝑋 → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) )
11 5 10 eqtrd ⊢ ( 𝐴 ∈ Word 𝑋 → ( 0 ..^ ( ♯ ‘ ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) )
12 11 adantr ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 0 ..^ ( ♯ ‘ ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) )
13 12 feq2d ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ) ) ⟶ 𝑋 ↔ ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) : ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ⟶ 𝑋 ) )
14 3 13 mpbid ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) : ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ⟶ 𝑋 )
15 14 ffnd ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) Fn ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) )
16 wrdf ⊢ ( 𝐴 ∈ Word 𝑋 → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑋 )
17 16 adantr ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑋 )
18 eqid ⊢ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } = { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ }
19 fsng ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝐵 ∈ 𝑋 ) → ( { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } : { ( ♯ ‘ 𝐴 ) } ⟶ { 𝐵 } ↔ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } = { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) )
20 18 19 mpbiri ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝐵 ∈ 𝑋 ) → { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } : { ( ♯ ‘ 𝐴 ) } ⟶ { 𝐵 } )
21 6 20 sylan ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } : { ( ♯ ‘ 𝐴 ) } ⟶ { 𝐵 } )
22 fzodisjsn ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∩ { ( ♯ ‘ 𝐴 ) } ) = ∅
23 22 a1i ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∩ { ( ♯ ‘ 𝐴 ) } ) = ∅ )
24 fun ⊢ ( ( ( 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑋 ∧ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } : { ( ♯ ‘ 𝐴 ) } ⟶ { 𝐵 } ) ∧ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∩ { ( ♯ ‘ 𝐴 ) } ) = ∅ ) → ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) : ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ⟶ ( 𝑋 ∪ { 𝐵 } ) )
25 17 21 23 24 syl21anc ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) : ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ⟶ ( 𝑋 ∪ { 𝐵 } ) )
26 25 ffnd ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) Fn ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) )
27 elun ⊢ ( 𝑥 ∈ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ↔ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∨ 𝑥 ∈ { ( ♯ ‘ 𝐴 ) } ) )
28 ccats1val1 ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
29 28 adantlr ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
30 simpr ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
31 fzonel ⊢ ¬ ( ♯ ‘ 𝐴 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) )
32 nelne2 ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑥 ≠ ( ♯ ‘ 𝐴 ) )
33 30 31 32 sylancl ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑥 ≠ ( ♯ ‘ 𝐴 ) )
34 33 necomd ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐴 ) ≠ 𝑥 )
35 fvunsn ⊢ ( ( ♯ ‘ 𝐴 ) ≠ 𝑥 → ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
36 34 35 syl ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
37 29 36 eqtr4d ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ 𝑥 ) = ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ 𝑥 ) )
38 fvexd ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ♯ ‘ 𝐴 ) ∈ V )
39 simpr ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
40 17 fdmd ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → dom 𝐴 = ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
41 40 eleq2d ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ♯ ‘ 𝐴 ) ∈ dom 𝐴 ↔ ( ♯ ‘ 𝐴 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) )
42 31 41 mtbiri ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ¬ ( ♯ ‘ 𝐴 ) ∈ dom 𝐴 )
43 fsnunfv ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ V ∧ 𝐵 ∈ 𝑋 ∧ ¬ ( ♯ ‘ 𝐴 ) ∈ dom 𝐴 ) → ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ ( ♯ ‘ 𝐴 ) ) = 𝐵 )
44 38 39 42 43 syl3anc ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ ( ♯ ‘ 𝐴 ) ) = 𝐵 )
45 simpl ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ Word 𝑋 )
46 s1cl ⊢ ( 𝐵 ∈ 𝑋 → ⟨“ 𝐵 ”⟩ ∈ Word 𝑋 )
47 46 adantl ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ⟨“ 𝐵 ”⟩ ∈ Word 𝑋 )
48 s1len ⊢ ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) = 1
49 1nn ⊢ 1 ∈ ℕ
50 48 49 eqeltri ⊢ ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) ∈ ℕ
51 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) ) ↔ ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) ∈ ℕ )
52 50 51 mpbir ⊢ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) )
53 52 a1i ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) ) )
54 ccatval3 ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ ⟨“ 𝐵 ”⟩ ∈ Word 𝑋 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐵 ”⟩ ) ) ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝐴 ) ) ) = ( ⟨“ 𝐵 ”⟩ ‘ 0 ) )
55 45 47 53 54 syl3anc ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝐴 ) ) ) = ( ⟨“ 𝐵 ”⟩ ‘ 0 ) )
56 s1fv ⊢ ( 𝐵 ∈ 𝑋 → ( ⟨“ 𝐵 ”⟩ ‘ 0 ) = 𝐵 )
57 56 adantl ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ⟨“ 𝐵 ”⟩ ‘ 0 ) = 𝐵 )
58 55 57 eqtrd ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝐴 ) ) ) = 𝐵 )
59 6 adantr ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
60 59 nn0cnd ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
61 60 addlidd ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 0 + ( ♯ ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )
62 61 fveq2d ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝐴 ) ) ) = ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ ( ♯ ‘ 𝐴 ) ) )
63 44 58 62 3eqtr2rd ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ ( ♯ ‘ 𝐴 ) ) )
64 elsni ⊢ ( 𝑥 ∈ { ( ♯ ‘ 𝐴 ) } → 𝑥 = ( ♯ ‘ 𝐴 ) )
65 64 fveq2d ⊢ ( 𝑥 ∈ { ( ♯ ‘ 𝐴 ) } → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ 𝑥 ) = ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ ( ♯ ‘ 𝐴 ) ) )
66 64 fveq2d ⊢ ( 𝑥 ∈ { ( ♯ ‘ 𝐴 ) } → ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ 𝑥 ) = ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ ( ♯ ‘ 𝐴 ) ) )
67 65 66 eqeq12d ⊢ ( 𝑥 ∈ { ( ♯ ‘ 𝐴 ) } → ( ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ 𝑥 ) = ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ 𝑥 ) ↔ ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
68 63 67 syl5ibrcom ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑥 ∈ { ( ♯ ‘ 𝐴 ) } → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ 𝑥 ) = ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ 𝑥 ) ) )
69 68 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 ∈ { ( ♯ ‘ 𝐴 ) } ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ 𝑥 ) = ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ 𝑥 ) )
70 37 69 jaodan ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∨ 𝑥 ∈ { ( ♯ ‘ 𝐴 ) } ) ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ 𝑥 ) = ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ 𝑥 ) )
71 27 70 sylan2b ⊢ ( ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝑥 ∈ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ) → ( ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) ‘ 𝑥 ) = ( ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) ‘ 𝑥 ) )
72 15 26 71 eqfnfvd ⊢ ( ( 𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ++ ⟨“ 𝐵 ”⟩ ) = ( 𝐴 ∪ { ⟨ ( ♯ ‘ 𝐴 ) , 𝐵 ⟩ } ) )