This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = (/) <-> ( A = (/) /\ B = (/) ) ) )

Proof

Step Hyp Ref Expression
1 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
2 1 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. A <-> A =/= (/) ) )
3 oaword1 
 |-  ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
4 3 sseld 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. A -> (/) e. ( A +o B ) ) )
5 2 4 sylbird 
 |-  ( ( A e. On /\ B e. On ) -> ( A =/= (/) -> (/) e. ( A +o B ) ) )
6 ne0i 
 |-  ( (/) e. ( A +o B ) -> ( A +o B ) =/= (/) )
7 5 6 syl6 
 |-  ( ( A e. On /\ B e. On ) -> ( A =/= (/) -> ( A +o B ) =/= (/) ) )
8 7 necon4d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = (/) -> A = (/) ) )
9 on0eln0 
 |-  ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
10 9 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. B <-> B =/= (/) ) )
11 0elon 
 |-  (/) e. On
12 oaord 
 |-  ( ( (/) e. On /\ B e. On /\ A e. On ) -> ( (/) e. B <-> ( A +o (/) ) e. ( A +o B ) ) )
13 11 12 mp3an1 
 |-  ( ( B e. On /\ A e. On ) -> ( (/) e. B <-> ( A +o (/) ) e. ( A +o B ) ) )
14 13 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. B <-> ( A +o (/) ) e. ( A +o B ) ) )
15 10 14 bitr3d 
 |-  ( ( A e. On /\ B e. On ) -> ( B =/= (/) <-> ( A +o (/) ) e. ( A +o B ) ) )
16 ne0i 
 |-  ( ( A +o (/) ) e. ( A +o B ) -> ( A +o B ) =/= (/) )
17 15 16 biimtrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( B =/= (/) -> ( A +o B ) =/= (/) ) )
18 17 necon4d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = (/) -> B = (/) ) )
19 8 18 jcad 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = (/) -> ( A = (/) /\ B = (/) ) ) )
20 oveq12 
 |-  ( ( A = (/) /\ B = (/) ) -> ( A +o B ) = ( (/) +o (/) ) )
21 oa0 
 |-  ( (/) e. On -> ( (/) +o (/) ) = (/) )
22 11 21 ax-mp 
 |-  ( (/) +o (/) ) = (/)
23 20 22 eqtrdi 
 |-  ( ( A = (/) /\ B = (/) ) -> ( A +o B ) = (/) )
24 19 23 impbid1 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = (/) <-> ( A = (/) /\ B = (/) ) ) )