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 𝐴 ) = 𝐴 )