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 
|- ( ( A e. On /\ B e. On ) -> ( ( B = (/) -> ( A ^o B ) = 1o ) /\ ( ( B = suc C /\ C e. On ) -> ( A ^o B ) = ( ( A ^o C ) .o A ) ) /\ ( Lim B -> ( A ^o B ) = if ( (/) e. A , U_ c e. B ( A ^o c ) , (/) ) ) ) )

Proof

Step Hyp Ref Expression
1 oe0 
 |-  ( A e. On -> ( A ^o (/) ) = 1o )
2 oesuc 
 |-  ( ( A e. On /\ C e. On ) -> ( A ^o suc C ) = ( ( A ^o C ) .o A ) )
3 oelim 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ c e. B ( A ^o c ) )
4 simpr 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ (/) e. A ) -> (/) e. A )
5 4 iftrued 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ (/) e. A ) -> if ( (/) e. A , U_ c e. B ( A ^o c ) , (/) ) = U_ c e. B ( A ^o c ) )
6 3 5 eqtr4d 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = if ( (/) e. A , U_ c e. B ( A ^o c ) , (/) ) )
7 simpl 
 |-  ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> A e. On )
8 0elon 
 |-  (/) e. On
9 ontri1 
 |-  ( ( A e. On /\ (/) e. On ) -> ( A C_ (/) <-> -. (/) e. A ) )
10 ss0 
 |-  ( A C_ (/) -> A = (/) )
11 9 10 syl6bir 
 |-  ( ( A e. On /\ (/) e. On ) -> ( -. (/) e. A -> A = (/) ) )
12 7 8 11 sylancl 
 |-  ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( -. (/) e. A -> A = (/) ) )
13 oveq1 
 |-  ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
14 oe0m1 
 |-  ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
15 14 biimpd 
 |-  ( B e. On -> ( (/) e. B -> ( (/) ^o B ) = (/) ) )
16 0ellim 
 |-  ( Lim B -> (/) e. B )
17 15 16 impel 
 |-  ( ( B e. On /\ Lim B ) -> ( (/) ^o B ) = (/) )
18 17 adantl 
 |-  ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( (/) ^o B ) = (/) )
19 13 18 sylan9eqr 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ A = (/) ) -> ( A ^o B ) = (/) )
20 19 ex 
 |-  ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( A = (/) -> ( A ^o B ) = (/) ) )
21 12 20 syld 
 |-  ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( -. (/) e. A -> ( A ^o B ) = (/) ) )
22 21 imp 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ -. (/) e. A ) -> ( A ^o B ) = (/) )
23 simpr 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ -. (/) e. A ) -> -. (/) e. A )
24 23 iffalsed 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ -. (/) e. A ) -> if ( (/) e. A , U_ c e. B ( A ^o c ) , (/) ) = (/) )
25 22 24 eqtr4d 
 |-  ( ( ( A e. On /\ ( B e. On /\ Lim B ) ) /\ -. (/) e. A ) -> ( A ^o B ) = if ( (/) e. A , U_ c e. B ( A ^o c ) , (/) ) )
26 6 25 pm2.61dan 
 |-  ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( A ^o B ) = if ( (/) e. A , U_ c e. B ( A ^o c ) , (/) ) )
27 26 anassrs 
 |-  ( ( ( A e. On /\ B e. On ) /\ Lim B ) -> ( A ^o B ) = if ( (/) e. A , U_ c e. B ( A ^o c ) , (/) ) )
28 1 2 27 onov0suclim 
 |-  ( ( A e. On /\ B e. On ) -> ( ( B = (/) -> ( A ^o B ) = 1o ) /\ ( ( B = suc C /\ C e. On ) -> ( A ^o B ) = ( ( A ^o C ) .o A ) ) /\ ( Lim B -> ( A ^o B ) = if ( (/) e. A , U_ c e. B ( A ^o c ) , (/) ) ) ) )