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}\in \mathrm{On}\to {1}_{𝑜}{\cdot }_{𝑜}{A}={A}$

Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{x}=\varnothing \to {1}_{𝑜}{\cdot }_{𝑜}{x}={1}_{𝑜}{\cdot }_{𝑜}\varnothing$
2 id ${⊢}{x}=\varnothing \to {x}=\varnothing$
3 1 2 eqeq12d ${⊢}{x}=\varnothing \to \left({1}_{𝑜}{\cdot }_{𝑜}{x}={x}↔{1}_{𝑜}{\cdot }_{𝑜}\varnothing =\varnothing \right)$
4 oveq2 ${⊢}{x}={y}\to {1}_{𝑜}{\cdot }_{𝑜}{x}={1}_{𝑜}{\cdot }_{𝑜}{y}$
5 id ${⊢}{x}={y}\to {x}={y}$
6 4 5 eqeq12d ${⊢}{x}={y}\to \left({1}_{𝑜}{\cdot }_{𝑜}{x}={x}↔{1}_{𝑜}{\cdot }_{𝑜}{y}={y}\right)$
7 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to {1}_{𝑜}{\cdot }_{𝑜}{x}={1}_{𝑜}{\cdot }_{𝑜}\mathrm{suc}{y}$
8 id ${⊢}{x}=\mathrm{suc}{y}\to {x}=\mathrm{suc}{y}$
9 7 8 eqeq12d ${⊢}{x}=\mathrm{suc}{y}\to \left({1}_{𝑜}{\cdot }_{𝑜}{x}={x}↔{1}_{𝑜}{\cdot }_{𝑜}\mathrm{suc}{y}=\mathrm{suc}{y}\right)$
10 oveq2 ${⊢}{x}={A}\to {1}_{𝑜}{\cdot }_{𝑜}{x}={1}_{𝑜}{\cdot }_{𝑜}{A}$
11 id ${⊢}{x}={A}\to {x}={A}$
12 10 11 eqeq12d ${⊢}{x}={A}\to \left({1}_{𝑜}{\cdot }_{𝑜}{x}={x}↔{1}_{𝑜}{\cdot }_{𝑜}{A}={A}\right)$
13 1on ${⊢}{1}_{𝑜}\in \mathrm{On}$
14 om0 ${⊢}{1}_{𝑜}\in \mathrm{On}\to {1}_{𝑜}{\cdot }_{𝑜}\varnothing =\varnothing$
15 13 14 ax-mp ${⊢}{1}_{𝑜}{\cdot }_{𝑜}\varnothing =\varnothing$
16 omsuc ${⊢}\left({1}_{𝑜}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to {1}_{𝑜}{\cdot }_{𝑜}\mathrm{suc}{y}=\left({1}_{𝑜}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{1}_{𝑜}$
17 13 16 mpan ${⊢}{y}\in \mathrm{On}\to {1}_{𝑜}{\cdot }_{𝑜}\mathrm{suc}{y}=\left({1}_{𝑜}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{1}_{𝑜}$
18 oveq1 ${⊢}{1}_{𝑜}{\cdot }_{𝑜}{y}={y}\to \left({1}_{𝑜}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{1}_{𝑜}={y}{+}_{𝑜}{1}_{𝑜}$
19 17 18 sylan9eq ${⊢}\left({y}\in \mathrm{On}\wedge {1}_{𝑜}{\cdot }_{𝑜}{y}={y}\right)\to {1}_{𝑜}{\cdot }_{𝑜}\mathrm{suc}{y}={y}{+}_{𝑜}{1}_{𝑜}$
20 oa1suc ${⊢}{y}\in \mathrm{On}\to {y}{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}{y}$
21 20 adantr ${⊢}\left({y}\in \mathrm{On}\wedge {1}_{𝑜}{\cdot }_{𝑜}{y}={y}\right)\to {y}{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}{y}$
22 19 21 eqtrd ${⊢}\left({y}\in \mathrm{On}\wedge {1}_{𝑜}{\cdot }_{𝑜}{y}={y}\right)\to {1}_{𝑜}{\cdot }_{𝑜}\mathrm{suc}{y}=\mathrm{suc}{y}$
23 22 ex ${⊢}{y}\in \mathrm{On}\to \left({1}_{𝑜}{\cdot }_{𝑜}{y}={y}\to {1}_{𝑜}{\cdot }_{𝑜}\mathrm{suc}{y}=\mathrm{suc}{y}\right)$
24 iuneq2 ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{1}_{𝑜}{\cdot }_{𝑜}{y}={y}\to \bigcup _{{y}\in {x}}\left({1}_{𝑜}{\cdot }_{𝑜}{y}\right)=\bigcup _{{y}\in {x}}{y}$
25 uniiun ${⊢}\bigcup {x}=\bigcup _{{y}\in {x}}{y}$
26 24 25 syl6eqr ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{1}_{𝑜}{\cdot }_{𝑜}{y}={y}\to \bigcup _{{y}\in {x}}\left({1}_{𝑜}{\cdot }_{𝑜}{y}\right)=\bigcup {x}$
27 vex ${⊢}{x}\in \mathrm{V}$
28 omlim ${⊢}\left({1}_{𝑜}\in \mathrm{On}\wedge \left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\right)\to {1}_{𝑜}{\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({1}_{𝑜}{\cdot }_{𝑜}{y}\right)$
29 13 28 mpan ${⊢}\left({x}\in \mathrm{V}\wedge \mathrm{Lim}{x}\right)\to {1}_{𝑜}{\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({1}_{𝑜}{\cdot }_{𝑜}{y}\right)$
30 27 29 mpan ${⊢}\mathrm{Lim}{x}\to {1}_{𝑜}{\cdot }_{𝑜}{x}=\bigcup _{{y}\in {x}}\left({1}_{𝑜}{\cdot }_{𝑜}{y}\right)$
31 limuni ${⊢}\mathrm{Lim}{x}\to {x}=\bigcup {x}$
32 30 31 eqeq12d ${⊢}\mathrm{Lim}{x}\to \left({1}_{𝑜}{\cdot }_{𝑜}{x}={x}↔\bigcup _{{y}\in {x}}\left({1}_{𝑜}{\cdot }_{𝑜}{y}\right)=\bigcup {x}\right)$
33 26 32 syl5ibr ${⊢}\mathrm{Lim}{x}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{1}_{𝑜}{\cdot }_{𝑜}{y}={y}\to {1}_{𝑜}{\cdot }_{𝑜}{x}={x}\right)$
34 3 6 9 12 15 23 33 tfinds ${⊢}{A}\in \mathrm{On}\to {1}_{𝑜}{\cdot }_{𝑜}{A}={A}$