Metamath Proof Explorer


Theorem oa0r

Description: Ordinal addition with zero. Proposition 8.3 of TakeutiZaring p. 57. (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 syl5ibr ( Lim 𝑥 → ( ∀ 𝑦𝑥 ( ∅ +o 𝑦 ) = 𝑦 → ( ∅ +o 𝑥 ) = 𝑥 ) )
31 3 6 9 12 15 20 30 tfinds ( 𝐴 ∈ On → ( ∅ +o 𝐴 ) = 𝐴 )