Metamath Proof Explorer


Theorem om1r

Description: Ordinal multiplication with 1. Proposition 8.18(2) of TakeutiZaring p. 63. (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 syl5ibr Lim x y x 1 𝑜 𝑜 y = y 1 𝑜 𝑜 x = x
34 3 6 9 12 15 23 33 tfinds A On 1 𝑜 𝑜 A = A