Metamath Proof Explorer


Theorem oa00

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 AOnBOnA+𝑜B=A=B=

Proof

Step Hyp Ref Expression
1 on0eln0 AOnAA
2 1 adantr AOnBOnAA
3 oaword1 AOnBOnAA+𝑜B
4 3 sseld AOnBOnAA+𝑜B
5 2 4 sylbird AOnBOnAA+𝑜B
6 ne0i A+𝑜BA+𝑜B
7 5 6 syl6 AOnBOnAA+𝑜B
8 7 necon4d AOnBOnA+𝑜B=A=
9 on0eln0 BOnBB
10 9 adantl AOnBOnBB
11 0elon On
12 oaord OnBOnAOnBA+𝑜A+𝑜B
13 11 12 mp3an1 BOnAOnBA+𝑜A+𝑜B
14 13 ancoms AOnBOnBA+𝑜A+𝑜B
15 10 14 bitr3d AOnBOnBA+𝑜A+𝑜B
16 ne0i A+𝑜A+𝑜BA+𝑜B
17 15 16 biimtrdi AOnBOnBA+𝑜B
18 17 necon4d AOnBOnA+𝑜B=B=
19 8 18 jcad AOnBOnA+𝑜B=A=B=
20 oveq12 A=B=A+𝑜B=+𝑜
21 oa0 On+𝑜=
22 11 21 ax-mp +𝑜=
23 20 22 eqtrdi A=B=A+𝑜B=
24 19 23 impbid1 AOnBOnA+𝑜B=A=B=