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 ๐ด ) = ๐ด )