Description: The value of a subword operation for inproper arguments is the empty set. (Contributed by AV, 2-Dec-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | swrdnd0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ianor | |
|
2 | 3ianor | |
|
3 | elfz2nn0 | |
|
4 | 2 3 | xchnxbir | |
5 | 3ianor | |
|
6 | elfz2nn0 | |
|
7 | 5 6 | xchnxbir | |
8 | 4 7 | orbi12i | |
9 | 1 8 | bitri | |
10 | df-3or | |
|
11 | ianor | |
|
12 | swrdnnn0nd | |
|
13 | 12 | expcom | |
14 | 11 13 | sylbir | |
15 | anor | |
|
16 | nn0re | |
|
17 | nn0re | |
|
18 | ltnle | |
|
19 | 16 17 18 | syl2anr | |
20 | nn0z | |
|
21 | nn0z | |
|
22 | 20 21 | anim12i | |
23 | 22 | anim2i | |
24 | 3anass | |
|
25 | 23 24 | sylibr | |
26 | 25 | adantr | |
27 | 17 16 | anim12ci | |
28 | 27 | adantl | |
29 | ltle | |
|
30 | 28 29 | syl | |
31 | 30 | imp | |
32 | 31 | 3mix2d | |
33 | swrdnd | |
|
34 | 26 32 33 | sylc | |
35 | 34 | ex | |
36 | 35 | expcom | |
37 | 36 | com23 | |
38 | 19 37 | sylbird | |
39 | 15 38 | sylbir | |
40 | 39 | imp | |
41 | 14 40 | jaoi3 | |
42 | 10 41 | sylbi | |
43 | 3anor | |
|
44 | pm2.24 | |
|
45 | 44 | 3ad2ant2 | |
46 | 45 | com12 | |
47 | pm2.24 | |
|
48 | lencl | |
|
49 | 47 48 | syl11 | |
50 | 49 | a1d | |
51 | 48 | nn0red | |
52 | 16 | 3ad2ant2 | |
53 | ltnle | |
|
54 | 51 52 53 | syl2anr | |
55 | simpr | |
|
56 | 20 | 3ad2ant1 | |
57 | 56 | adantr | |
58 | 21 | 3ad2ant2 | |
59 | 58 | adantr | |
60 | 55 57 59 | 3jca | |
61 | 3mix3 | |
|
62 | 60 61 33 | syl2im | |
63 | 54 62 | sylbird | |
64 | 63 | com12 | |
65 | 64 | expd | |
66 | 46 50 65 | 3jaoi | |
67 | 43 66 | syl5bir | |
68 | 67 | impcom | |
69 | 42 68 | jaoi3 | |
70 | 69 | com12 | |
71 | 9 70 | syl5bi | |