Theorem oa00

Description: An ordinal sum is zero iff both of its arguments are zero. (Contributed by NM, 6-Dec-2004)

	Ref	Expression
Assertion	oa00	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		on0eln0	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
3		oaword1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐴 +o 𝐵 ) )
4	3	sseld	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐴 → ∅ ∈ ( 𝐴 +o 𝐵 ) ) )
5	2 4	sylbird	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ≠ ∅ → ∅ ∈ ( 𝐴 +o 𝐵 ) ) )
6		ne0i	⊢ ( ∅ ∈ ( 𝐴 +o 𝐵 ) → ( 𝐴 +o 𝐵 ) ≠ ∅ )
7	5 6	syl6	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ≠ ∅ → ( 𝐴 +o 𝐵 ) ≠ ∅ ) )
8	7	necon4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) = ∅ → 𝐴 = ∅ ) )
9		on0eln0	⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) )
10	9	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) )
11		0elon	⊢ ∅ ∈ On
12		oaord	⊢ ( ( ∅ ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐵 ↔ ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝐵 ) ) )
13	11 12	mp3an1	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ∈ 𝐵 ↔ ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝐵 ) ) )
14	13	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐵 ↔ ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝐵 ) ) )
15	10 14	bitr3d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ≠ ∅ ↔ ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝐵 ) ) )
16		ne0i	⊢ ( ( 𝐴 +o ∅ ) ∈ ( 𝐴 +o 𝐵 ) → ( 𝐴 +o 𝐵 ) ≠ ∅ )
17	15 16	syl6bi	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ≠ ∅ → ( 𝐴 +o 𝐵 ) ≠ ∅ ) )
18	17	necon4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) = ∅ → 𝐵 = ∅ ) )
19	8 18	jcad	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) = ∅ → ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
20		oveq12	⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → ( 𝐴 +o 𝐵 ) = ( ∅ +o ∅ ) )
21		oa0	⊢ ( ∅ ∈ On → ( ∅ +o ∅ ) = ∅ )
22	11 21	ax-mp	⊢ ( ∅ +o ∅ ) = ∅
23	20 22	eqtrdi	⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → ( 𝐴 +o 𝐵 ) = ∅ )
24	19 23	impbid1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )