Description: If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2mpo0.o | |
|
2mpo0.u | |
||
Assertion | 2mpo0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2mpo0.o | |
|
2 | 2mpo0.u | |
|
3 | ianor | |
|
4 | 1 | mpondm0 | |
5 | 4 | oveqd | |
6 | 0ov | |
|
7 | 5 6 | eqtrdi | |
8 | notnotb | |
|
9 | 2 | adantr | |
10 | 9 | oveqd | |
11 | eqid | |
|
12 | 11 | mpondm0 | |
13 | 12 | adantl | |
14 | 10 13 | eqtrd | |
15 | 8 14 | sylanbr | |
16 | 7 15 | jaoi3 | |
17 | 3 16 | sylbi | |