Metamath Proof Explorer

Theorem oe0suclim

Description: Closed form expression of the value of ordinal exponentiation for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.6 of Schloeder p. 4. See oe0 , oesuc , oe0m1 , and oelim . (Contributed by RP, 18-Jan-2025)

Ref Expression
Assertion oe0suclim ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ → ( 𝐴 ↑o 𝐵 ) = 1o ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐵 ) = ( ( 𝐴 ↑o 𝐶 ) ·o 𝐴 ) ) ∧ ( Lim 𝐵 → ( 𝐴 ↑o 𝐵 ) = if ( ∅ ∈ 𝐴 , ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) , ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 oe0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) = 1o )
2 oesuc ⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o suc 𝐶 ) = ( ( 𝐴 ↑o 𝐶 ) ·o 𝐴 ) )
3 oelim ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) )
4 simpr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ∅ ∈ 𝐴 )
5 4 iftrued ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → if ( ∅ ∈ 𝐴 , ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) , ∅ ) = ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) )
6 3 5 eqtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = if ( ∅ ∈ 𝐴 , ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) , ∅ ) )
7 simpl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → 𝐴 ∈ On )
8 0elon ⊢ ∅ ∈ On
9 ontri1 ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ On ) → ( 𝐴 ⊆ ∅ ↔ ¬ ∅ ∈ 𝐴 ) )
10 ss0 ⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
11 9 10 biimtrrdi ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ On ) → ( ¬ ∅ ∈ 𝐴 → 𝐴 = ∅ ) )
12 7 8 11 sylancl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( ¬ ∅ ∈ 𝐴 → 𝐴 = ∅ ) )
13 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ( ∅ ↑o 𝐵 ) )
14 oe0m1 ⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) )
15 14 biimpd ⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 → ( ∅ ↑o 𝐵 ) = ∅ ) )
16 0ellim ⊢ ( Lim 𝐵 → ∅ ∈ 𝐵 )
17 15 16 impel ⊢ ( ( 𝐵 ∈ On ∧ Lim 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ )
18 17 adantl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( ∅ ↑o 𝐵 ) = ∅ )
19 13 18 sylan9eqr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ∅ )
20 19 ex ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ∅ ) )
21 12 20 syld ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( ¬ ∅ ∈ 𝐴 → ( 𝐴 ↑o 𝐵 ) = ∅ ) )
22 21 imp ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ¬ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ∅ )
23 simpr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ¬ ∅ ∈ 𝐴 ) → ¬ ∅ ∈ 𝐴 )
24 23 iffalsed ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ¬ ∅ ∈ 𝐴 ) → if ( ∅ ∈ 𝐴 , ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) , ∅ ) = ∅ )
25 22 24 eqtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) ∧ ¬ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = if ( ∅ ∈ 𝐴 , ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) , ∅ ) )
26 6 25 pm2.61dan ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ Lim 𝐵 ) ) → ( 𝐴 ↑o 𝐵 ) = if ( ∅ ∈ 𝐴 , ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) , ∅ ) )
27 26 anassrs ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ Lim 𝐵 ) → ( 𝐴 ↑o 𝐵 ) = if ( ∅ ∈ 𝐴 , ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) , ∅ ) )
28 1 2 27 onov0suclim ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 = ∅ → ( 𝐴 ↑o 𝐵 ) = 1o ) ∧ ( ( 𝐵 = suc 𝐶 ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐵 ) = ( ( 𝐴 ↑o 𝐶 ) ·o 𝐴 ) ) ∧ ( Lim 𝐵 → ( 𝐴 ↑o 𝐵 ) = if ( ∅ ∈ 𝐴 , ∪ 𝑐 ∈ 𝐵 ( 𝐴 ↑o 𝑐 ) , ∅ ) ) ) )