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 = (/) ) ) )