Metamath Proof Explorer

Theorem om1r

Description: Ordinal multiplication with 1. Proposition 8.18(2) of TakeutiZaring p. 63. Lemma 2.15 of Schloeder p. 5. (Contributed by NM, 3-Aug-2004)

Ref Expression
Assertion om1r ⊢ A ∈ On → 1 𝑜 ⋅ 𝑜 A = A

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ x = ∅ → 1 𝑜 ⋅ 𝑜 x = 1 𝑜 ⋅ 𝑜 ∅
2 id ⊢ x = ∅ → x = ∅
3 1 2 eqeq12d ⊢ x = ∅ → 1 𝑜 ⋅ 𝑜 x = x ↔ 1 𝑜 ⋅ 𝑜 ∅ = ∅
4 oveq2 ⊢ x = y → 1 𝑜 ⋅ 𝑜 x = 1 𝑜 ⋅ 𝑜 y
5 id ⊢ x = y → x = y
6 4 5 eqeq12d ⊢ x = y → 1 𝑜 ⋅ 𝑜 x = x ↔ 1 𝑜 ⋅ 𝑜 y = y
7 oveq2 ⊢ x = suc ⁡ y → 1 𝑜 ⋅ 𝑜 x = 1 𝑜 ⋅ 𝑜 suc ⁡ y
8 id ⊢ x = suc ⁡ y → x = suc ⁡ y
9 7 8 eqeq12d ⊢ x = suc ⁡ y → 1 𝑜 ⋅ 𝑜 x = x ↔ 1 𝑜 ⋅ 𝑜 suc ⁡ y = suc ⁡ y
10 oveq2 ⊢ x = A → 1 𝑜 ⋅ 𝑜 x = 1 𝑜 ⋅ 𝑜 A
11 id ⊢ x = A → x = A
12 10 11 eqeq12d ⊢ x = A → 1 𝑜 ⋅ 𝑜 x = x ↔ 1 𝑜 ⋅ 𝑜 A = A
13 1on ⊢ 1 𝑜 ∈ On
14 om0 ⊢ 1 𝑜 ∈ On → 1 𝑜 ⋅ 𝑜 ∅ = ∅
15 13 14 ax-mp ⊢ 1 𝑜 ⋅ 𝑜 ∅ = ∅
16 omsuc ⊢ 1 𝑜 ∈ On ∧ y ∈ On → 1 𝑜 ⋅ 𝑜 suc ⁡ y = 1 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜
17 13 16 mpan ⊢ y ∈ On → 1 𝑜 ⋅ 𝑜 suc ⁡ y = 1 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜
18 oveq1 ⊢ 1 𝑜 ⋅ 𝑜 y = y → 1 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜 = y + 𝑜 1 𝑜
19 17 18 sylan9eq ⊢ y ∈ On ∧ 1 𝑜 ⋅ 𝑜 y = y → 1 𝑜 ⋅ 𝑜 suc ⁡ y = y + 𝑜 1 𝑜
20 oa1suc ⊢ y ∈ On → y + 𝑜 1 𝑜 = suc ⁡ y
21 20 adantr ⊢ y ∈ On ∧ 1 𝑜 ⋅ 𝑜 y = y → y + 𝑜 1 𝑜 = suc ⁡ y
22 19 21 eqtrd ⊢ y ∈ On ∧ 1 𝑜 ⋅ 𝑜 y = y → 1 𝑜 ⋅ 𝑜 suc ⁡ y = suc ⁡ y
23 22 ex ⊢ y ∈ On → 1 𝑜 ⋅ 𝑜 y = y → 1 𝑜 ⋅ 𝑜 suc ⁡ y = suc ⁡ y
24 iuneq2 ⊢ ∀ y ∈ x 1 𝑜 ⋅ 𝑜 y = y → ⋃ y ∈ x 1 𝑜 ⋅ 𝑜 y = ⋃ y ∈ x y
25 uniiun ⊢ ⋃ x = ⋃ y ∈ x y
26 24 25 eqtr4di ⊢ ∀ y ∈ x 1 𝑜 ⋅ 𝑜 y = y → ⋃ y ∈ x 1 𝑜 ⋅ 𝑜 y = ⋃ x
27 vex ⊢ x ∈ V
28 omlim ⊢ 1 𝑜 ∈ On ∧ x ∈ V ∧ Lim ⁡ x → 1 𝑜 ⋅ 𝑜 x = ⋃ y ∈ x 1 𝑜 ⋅ 𝑜 y
29 13 28 mpan ⊢ x ∈ V ∧ Lim ⁡ x → 1 𝑜 ⋅ 𝑜 x = ⋃ y ∈ x 1 𝑜 ⋅ 𝑜 y
30 27 29 mpan ⊢ Lim ⁡ x → 1 𝑜 ⋅ 𝑜 x = ⋃ y ∈ x 1 𝑜 ⋅ 𝑜 y
31 limuni ⊢ Lim ⁡ x → x = ⋃ x
32 30 31 eqeq12d ⊢ Lim ⁡ x → 1 𝑜 ⋅ 𝑜 x = x ↔ ⋃ y ∈ x 1 𝑜 ⋅ 𝑜 y = ⋃ x
33 26 32 imbitrrid ⊢ Lim ⁡ x → ∀ y ∈ x 1 𝑜 ⋅ 𝑜 y = y → 1 𝑜 ⋅ 𝑜 x = x
34 3 6 9 12 15 23 33 tfinds ⊢ A ∈ On → 1 𝑜 ⋅ 𝑜 A = A