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

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 ( 𝐴 ∈ On → ( 1o ·o 𝐴 ) = 𝐴 )

Proof

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