Metamath Proof Explorer

Theorem oevn0

Description: Value of ordinal exponentiation at a nonzero base. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oevn0 
|- ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( A ^o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )

Proof

Step Hyp Ref Expression
1 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
2 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
3 1 2 bitrdi 
 |-  ( A e. On -> ( (/) e. A <-> -. A = (/) ) )
4 3 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. A <-> -. A = (/) ) )
5 oev 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) = if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
6 iffalse 
 |-  ( -. A = (/) -> if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )
7 5 6 sylan9eq 
 |-  ( ( ( A e. On /\ B e. On ) /\ -. A = (/) ) -> ( A ^o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )
8 7 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( -. A = (/) -> ( A ^o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
9 4 8 sylbid 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. A -> ( A ^o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
10 9 imp 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( A ^o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )