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

Metamath Proof Explorer

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 𝐴 ) = 𝐴 )