This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oe1m

Description: Ordinal exponentiation with a base of 1. Proposition 8.31(3) of TakeutiZaring p. 67. Lemma 2.17 of Schloeder p. 6. (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 eqtrdi ⊢ ( ( 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 imbitrrid ⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 1o ↑o 𝑦 ) = 1o → ( 1o ↑o 𝑥 ) = 1o ) )
35 2 4 6 8 11 19 34 tfinds ⊢ ( 𝐴 ∈ On → ( 1o ↑o 𝐴 ) = 1o )