Metamath Proof Explorer

Theorem oe0m

Description: Value of zero raised to an ordinal. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oe0m 
|- ( A e. On -> ( (/) ^o A ) = ( 1o \ A ) )

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 oev 
 |-  ( ( (/) e. On /\ A e. On ) -> ( (/) ^o A ) = if ( (/) = (/) , ( 1o \ A ) , ( rec ( ( x e. _V |-> ( x .o (/) ) ) , 1o ) ` A ) ) )
3 1 2 mpan 
 |-  ( A e. On -> ( (/) ^o A ) = if ( (/) = (/) , ( 1o \ A ) , ( rec ( ( x e. _V |-> ( x .o (/) ) ) , 1o ) ` A ) ) )
4 eqid 
 |-  (/) = (/)
5 4 iftruei 
 |-  if ( (/) = (/) , ( 1o \ A ) , ( rec ( ( x e. _V |-> ( x .o (/) ) ) , 1o ) ` A ) ) = ( 1o \ A )
6 3 5 eqtrdi 
 |-  ( A e. On -> ( (/) ^o A ) = ( 1o \ A ) )