Theorem oa0r

Description: Ordinal addition with zero. Proposition 8.3 of TakeutiZaring p. 57. Lemma 2.14 of Schloeder p. 5. (Contributed by NM, 5-May-1995)

	Ref	Expression
Assertion	oa0r	⊢ ( 𝐴 ∈ On → ( ∅ +o 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = ∅ → ( ∅ +o 𝑥 ) = ( ∅ +o ∅ ) )
2		id	⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
3	1 2	eqeq12d	⊢ ( 𝑥 = ∅ → ( ( ∅ +o 𝑥 ) = 𝑥 ↔ ( ∅ +o ∅ ) = ∅ ) )
4		oveq2	⊢ ( 𝑥 = 𝑦 → ( ∅ +o 𝑥 ) = ( ∅ +o 𝑦 ) )
5		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
6	4 5	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( ∅ +o 𝑥 ) = 𝑥 ↔ ( ∅ +o 𝑦 ) = 𝑦 ) )
7		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( ∅ +o 𝑥 ) = ( ∅ +o suc 𝑦 ) )
8		id	⊢ ( 𝑥 = suc 𝑦 → 𝑥 = suc 𝑦 )
9	7 8	eqeq12d	⊢ ( 𝑥 = suc 𝑦 → ( ( ∅ +o 𝑥 ) = 𝑥 ↔ ( ∅ +o suc 𝑦 ) = suc 𝑦 ) )
10		oveq2	⊢ ( 𝑥 = 𝐴 → ( ∅ +o 𝑥 ) = ( ∅ +o 𝐴 ) )
11		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
12	10 11	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( ∅ +o 𝑥 ) = 𝑥 ↔ ( ∅ +o 𝐴 ) = 𝐴 ) )
13		0elon	⊢ ∅ ∈ On
14		oa0	⊢ ( ∅ ∈ On → ( ∅ +o ∅ ) = ∅ )
15	13 14	ax-mp	⊢ ( ∅ +o ∅ ) = ∅
16		oasuc	⊢ ( ( ∅ ∈ On ∧ 𝑦 ∈ On ) → ( ∅ +o suc 𝑦 ) = suc ( ∅ +o 𝑦 ) )
17	13 16	mpan	⊢ ( 𝑦 ∈ On → ( ∅ +o suc 𝑦 ) = suc ( ∅ +o 𝑦 ) )
18		suceq	⊢ ( ( ∅ +o 𝑦 ) = 𝑦 → suc ( ∅ +o 𝑦 ) = suc 𝑦 )
19	17 18	sylan9eq	⊢ ( ( 𝑦 ∈ On ∧ ( ∅ +o 𝑦 ) = 𝑦 ) → ( ∅ +o suc 𝑦 ) = suc 𝑦 )
20	19	ex	⊢ ( 𝑦 ∈ On → ( ( ∅ +o 𝑦 ) = 𝑦 → ( ∅ +o suc 𝑦 ) = suc 𝑦 ) )
21		iuneq2	⊢ ( ∀ 𝑦 ∈ 𝑥 ( ∅ +o 𝑦 ) = 𝑦 → ∪ 𝑦 ∈ 𝑥 ( ∅ +o 𝑦 ) = ∪ 𝑦 ∈ 𝑥 𝑦 )
22		uniiun	⊢ ∪ 𝑥 = ∪ 𝑦 ∈ 𝑥 𝑦
23	21 22	eqtr4di	⊢ ( ∀ 𝑦 ∈ 𝑥 ( ∅ +o 𝑦 ) = 𝑦 → ∪ 𝑦 ∈ 𝑥 ( ∅ +o 𝑦 ) = ∪ 𝑥 )
24		vex	⊢ 𝑥 ∈ V
25		oalim	⊢ ( ( ∅ ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( ∅ +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ∅ +o 𝑦 ) )
26	13 25	mpan	⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( ∅ +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ∅ +o 𝑦 ) )
27	24 26	mpan	⊢ ( Lim 𝑥 → ( ∅ +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ∅ +o 𝑦 ) )
28		limuni	⊢ ( Lim 𝑥 → 𝑥 = ∪ 𝑥 )
29	27 28	eqeq12d	⊢ ( Lim 𝑥 → ( ( ∅ +o 𝑥 ) = 𝑥 ↔ ∪ 𝑦 ∈ 𝑥 ( ∅ +o 𝑦 ) = ∪ 𝑥 ) )
30	23 29	imbitrrid	⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( ∅ +o 𝑦 ) = 𝑦 → ( ∅ +o 𝑥 ) = 𝑥 ) )
31	3 6 9 12 15 20 30	tfinds	⊢ ( 𝐴 ∈ On → ( ∅ +o 𝐴 ) = 𝐴 )