Description: An ordinal sum is zero iff both of its arguments are zero. Lemma 3.10 of Schloeder p. 8. (Contributed by NM, 6-Dec-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | oa00 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | on0eln0 | |
|
2 | 1 | adantr | |
3 | oaword1 | |
|
4 | 3 | sseld | |
5 | 2 4 | sylbird | |
6 | ne0i | |
|
7 | 5 6 | syl6 | |
8 | 7 | necon4d | |
9 | on0eln0 | |
|
10 | 9 | adantl | |
11 | 0elon | |
|
12 | oaord | |
|
13 | 11 12 | mp3an1 | |
14 | 13 | ancoms | |
15 | 10 14 | bitr3d | |
16 | ne0i | |
|
17 | 15 16 | biimtrdi | |
18 | 17 | necon4d | |
19 | 8 18 | jcad | |
20 | oveq12 | |
|
21 | oa0 | |
|
22 | 11 21 | ax-mp | |
23 | 20 22 | eqtrdi | |
24 | 19 23 | impbid1 | |