Theorem oe0

Description: Ordinal exponentiation with zero exponent. Definition 8.30 of TakeutiZaring p. 67. Definition 2.6 of Schloeder p. 4. (Contributed by NM, 31-Dec-2004) (Revised by Mario Carneiro, 8-Sep-2013)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	|- ( A = (/) -> ( A ^o (/) ) = ( (/) ^o (/) ) )
2		oe0m0	|- ( (/) ^o (/) ) = 1o
3	1 2	eqtrdi	|- ( A = (/) -> ( A ^o (/) ) = 1o )
4	3	adantl	|- ( ( A e. On /\ A = (/) ) -> ( A ^o (/) ) = 1o )
5		0elon	|- (/) e. On
6		oevn0	|- ( ( ( A e. On /\ (/) e. On ) /\ (/) e. A ) -> ( A ^o (/) ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` (/) ) )
7	5 6	mpanl2	|- ( ( A e. On /\ (/) e. A ) -> ( A ^o (/) ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` (/) ) )
8		1oex	|- 1o e. _V
9	8	rdg0	|- ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` (/) ) = 1o
10	7 9	eqtrdi	|- ( ( A e. On /\ (/) e. A ) -> ( A ^o (/) ) = 1o )
11	10	adantll	|- ( ( ( A e. On /\ A e. On ) /\ (/) e. A ) -> ( A ^o (/) ) = 1o )
12	4 11	oe0lem	|- ( ( A e. On /\ A e. On ) -> ( A ^o (/) ) = 1o )
13	12	anidms	|- ( A e. On -> ( A ^o (/) ) = 1o )