Theorem oe0rif

Description: Ordinal zero raised to any non-zero ordinal power is zero and zero to the zeroth power is one. Lemma 2.18 of Schloeder p. 6. (Contributed by RP, 29-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oe0m	|- ( A e. On -> ( (/) ^o A ) = ( 1o \ A ) )
2		nel02	|- ( A = (/) -> -. (/) e. A )
3	2	iffalsed	|- ( A = (/) -> if ( (/) e. A , (/) , 1o ) = 1o )
4		difeq2	|- ( A = (/) -> ( 1o \ A ) = ( 1o \ (/) ) )
5		dif0	|- ( 1o \ (/) ) = 1o
6	4 5	eqtrdi	|- ( A = (/) -> ( 1o \ A ) = 1o )
7	3 6	eqtr4d	|- ( A = (/) -> if ( (/) e. A , (/) , 1o ) = ( 1o \ A ) )
8	7	adantl	|- ( ( A e. On /\ A = (/) ) -> if ( (/) e. A , (/) , 1o ) = ( 1o \ A ) )
9		iftrue	|- ( (/) e. A -> if ( (/) e. A , (/) , 1o ) = (/) )
10	9	adantl	|- ( ( A e. On /\ (/) e. A ) -> if ( (/) e. A , (/) , 1o ) = (/) )
11		eloni	|- ( A e. On -> Ord A )
12		ordgt0ge1	|- ( Ord A -> ( (/) e. A <-> 1o C_ A ) )
13	11 12	syl	|- ( A e. On -> ( (/) e. A <-> 1o C_ A ) )
14	13	biimpa	|- ( ( A e. On /\ (/) e. A ) -> 1o C_ A )
15		ssdif0	|- ( 1o C_ A <-> ( 1o \ A ) = (/) )
16	14 15	sylib	|- ( ( A e. On /\ (/) e. A ) -> ( 1o \ A ) = (/) )
17	10 16	eqtr4d	|- ( ( A e. On /\ (/) e. A ) -> if ( (/) e. A , (/) , 1o ) = ( 1o \ A ) )
18		on0eqel	|- ( A e. On -> ( A = (/) \/ (/) e. A ) )
19	8 17 18	mpjaodan	|- ( A e. On -> if ( (/) e. A , (/) , 1o ) = ( 1o \ A ) )
20	1 19	eqtr4d	|- ( A e. On -> ( (/) ^o A ) = if ( (/) e. A , (/) , 1o ) )