Theorem oe1m

Description: Ordinal exponentiation with a mantissa of 1. Proposition 8.31(3) of TakeutiZaring p. 67. (Contributed by NM, 2-Jan-2005)

	Ref	Expression
Assertion	oe1m	⊢ ( 𝐴 ∈ On → ( 1o ↑o 𝐴 ) = 1o )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = ∅ → ( 1o ↑o 𝑥 ) = ( 1o ↑o ∅ ) )
2	1	eqeq1d	⊢ ( 𝑥 = ∅ → ( ( 1o ↑o 𝑥 ) = 1o ↔ ( 1o ↑o ∅ ) = 1o ) )
3		oveq2	⊢ ( 𝑥 = 𝑦 → ( 1o ↑o 𝑥 ) = ( 1o ↑o 𝑦 ) )
4	3	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 1o ↑o 𝑥 ) = 1o ↔ ( 1o ↑o 𝑦 ) = 1o ) )
5		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( 1o ↑o 𝑥 ) = ( 1o ↑o suc 𝑦 ) )
6	5	eqeq1d	⊢ ( 𝑥 = suc 𝑦 → ( ( 1o ↑o 𝑥 ) = 1o ↔ ( 1o ↑o suc 𝑦 ) = 1o ) )
7		oveq2	⊢ ( 𝑥 = 𝐴 → ( 1o ↑o 𝑥 ) = ( 1o ↑o 𝐴 ) )
8	7	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 1o ↑o 𝑥 ) = 1o ↔ ( 1o ↑o 𝐴 ) = 1o ) )
9		1on	⊢ 1o ∈ On
10		oe0	⊢ ( 1o ∈ On → ( 1o ↑o ∅ ) = 1o )
11	9 10	ax-mp	⊢ ( 1o ↑o ∅ ) = 1o
12		oesuc	⊢ ( ( 1o ∈ On ∧ 𝑦 ∈ On ) → ( 1o ↑o suc 𝑦 ) = ( ( 1o ↑o 𝑦 ) ·o 1o ) )
13	9 12	mpan	⊢ ( 𝑦 ∈ On → ( 1o ↑o suc 𝑦 ) = ( ( 1o ↑o 𝑦 ) ·o 1o ) )
14		oveq1	⊢ ( ( 1o ↑o 𝑦 ) = 1o → ( ( 1o ↑o 𝑦 ) ·o 1o ) = ( 1o ·o 1o ) )
15		om1	⊢ ( 1o ∈ On → ( 1o ·o 1o ) = 1o )
16	9 15	ax-mp	⊢ ( 1o ·o 1o ) = 1o
17	14 16	syl6eq	⊢ ( ( 1o ↑o 𝑦 ) = 1o → ( ( 1o ↑o 𝑦 ) ·o 1o ) = 1o )
18	13 17	sylan9eq	⊢ ( ( 𝑦 ∈ On ∧ ( 1o ↑o 𝑦 ) = 1o ) → ( 1o ↑o suc 𝑦 ) = 1o )
19	18	ex	⊢ ( 𝑦 ∈ On → ( ( 1o ↑o 𝑦 ) = 1o → ( 1o ↑o suc 𝑦 ) = 1o ) )
20		iuneq2	⊢ ( ∀ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) = 1o → ∪ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) = ∪ 𝑦 ∈ 𝑥 1o )
21		vex	⊢ 𝑥 ∈ V
22		0lt1o	⊢ ∅ ∈ 1o
23		oelim	⊢ ( ( ( 1o ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) ∧ ∅ ∈ 1o ) → ( 1o ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) )
24	22 23	mpan2	⊢ ( ( 1o ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 1o ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) )
25	9 24	mpan	⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( 1o ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) )
26	21 25	mpan	⊢ ( Lim 𝑥 → ( 1o ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) )
27	26	eqeq1d	⊢ ( Lim 𝑥 → ( ( 1o ↑o 𝑥 ) = 1o ↔ ∪ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) = 1o ) )
28		0ellim	⊢ ( Lim 𝑥 → ∅ ∈ 𝑥 )
29		ne0i	⊢ ( ∅ ∈ 𝑥 → 𝑥 ≠ ∅ )
30		iunconst	⊢ ( 𝑥 ≠ ∅ → ∪ 𝑦 ∈ 𝑥 1o = 1o )
31	28 29 30	3syl	⊢ ( Lim 𝑥 → ∪ 𝑦 ∈ 𝑥 1o = 1o )
32	31	eqeq2d	⊢ ( Lim 𝑥 → ( ∪ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) = ∪ 𝑦 ∈ 𝑥 1o ↔ ∪ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) = 1o ) )
33	27 32	bitr4d	⊢ ( Lim 𝑥 → ( ( 1o ↑o 𝑥 ) = 1o ↔ ∪ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) = ∪ 𝑦 ∈ 𝑥 1o ) )
34	20 33	syl5ibr	⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) = 1o → ( 1o ↑o 𝑥 ) = 1o ) )
35	2 4 6 8 11 19 34	tfinds	⊢ ( 𝐴 ∈ On → ( 1o ↑o 𝐴 ) = 1o )