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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccatws1cl | |
|
2 | wrdf | |
|
3 | 1 2 | syl | |
4 | ccatws1len | |
|
5 | 4 | oveq2d | |
6 | lencl | |
|
7 | nn0uz | |
|
8 | 6 7 | eleqtrdi | |
9 | fzosplitsn | |
|
10 | 8 9 | syl | |
11 | 5 10 | eqtrd | |
12 | 11 | adantr | |
13 | 12 | feq2d | |
14 | 3 13 | mpbid | |
15 | 14 | ffnd | |
16 | wrdf | |
|
17 | 16 | adantr | |
18 | eqid | |
|
19 | fsng | |
|
20 | 18 19 | mpbiri | |
21 | 6 20 | sylan | |
22 | fzodisjsn | |
|
23 | 22 | a1i | |
24 | fun | |
|
25 | 17 21 23 24 | syl21anc | |
26 | 25 | ffnd | |
27 | elun | |
|
28 | ccats1val1 | |
|
29 | 28 | adantlr | |
30 | simpr | |
|
31 | fzonel | |
|
32 | nelne2 | |
|
33 | 30 31 32 | sylancl | |
34 | 33 | necomd | |
35 | fvunsn | |
|
36 | 34 35 | syl | |
37 | 29 36 | eqtr4d | |
38 | fvexd | |
|
39 | simpr | |
|
40 | 17 | fdmd | |
41 | 40 | eleq2d | |
42 | 31 41 | mtbiri | |
43 | fsnunfv | |
|
44 | 38 39 42 43 | syl3anc | |
45 | simpl | |
|
46 | s1cl | |
|
47 | 46 | adantl | |
48 | s1len | |
|
49 | 1nn | |
|
50 | 48 49 | eqeltri | |
51 | lbfzo0 | |
|
52 | 50 51 | mpbir | |
53 | 52 | a1i | |
54 | ccatval3 | |
|
55 | 45 47 53 54 | syl3anc | |
56 | s1fv | |
|
57 | 56 | adantl | |
58 | 55 57 | eqtrd | |
59 | 6 | adantr | |
60 | 59 | nn0cnd | |
61 | 60 | addid2d | |
62 | 61 | fveq2d | |
63 | 44 58 62 | 3eqtr2rd | |
64 | elsni | |
|
65 | 64 | fveq2d | |
66 | 64 | fveq2d | |
67 | 65 66 | eqeq12d | |
68 | 63 67 | syl5ibrcom | |
69 | 68 | imp | |
70 | 37 69 | jaodan | |
71 | 27 70 | sylan2b | |
72 | 15 26 71 | eqfnfvd | |