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	⊢ ( 𝐴 ∈ On → ( ∅ ↑o 𝐴 ) = if ( ∅ ∈ 𝐴 , ∅ , 1o ) )

Proof

Step	Hyp	Ref	Expression
1		oe0m	⊢ ( 𝐴 ∈ On → ( ∅ ↑o 𝐴 ) = ( 1o ∖ 𝐴 ) )
2		nel02	⊢ ( 𝐴 = ∅ → ¬ ∅ ∈ 𝐴 )
3	2	iffalsed	⊢ ( 𝐴 = ∅ → if ( ∅ ∈ 𝐴 , ∅ , 1o ) = 1o )
4		difeq2	⊢ ( 𝐴 = ∅ → ( 1o ∖ 𝐴 ) = ( 1o ∖ ∅ ) )
5		dif0	⊢ ( 1o ∖ ∅ ) = 1o
6	4 5	eqtrdi	⊢ ( 𝐴 = ∅ → ( 1o ∖ 𝐴 ) = 1o )
7	3 6	eqtr4d	⊢ ( 𝐴 = ∅ → if ( ∅ ∈ 𝐴 , ∅ , 1o ) = ( 1o ∖ 𝐴 ) )
8	7	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = ∅ ) → if ( ∅ ∈ 𝐴 , ∅ , 1o ) = ( 1o ∖ 𝐴 ) )
9		iftrue	⊢ ( ∅ ∈ 𝐴 → if ( ∅ ∈ 𝐴 , ∅ , 1o ) = ∅ )
10	9	adantl	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → if ( ∅ ∈ 𝐴 , ∅ , 1o ) = ∅ )
11		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
12		ordgt0ge1	⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
13	11 12	syl	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
14	13	biimpa	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → 1o ⊆ 𝐴 )
15		ssdif0	⊢ ( 1o ⊆ 𝐴 ↔ ( 1o ∖ 𝐴 ) = ∅ )
16	14 15	sylib	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( 1o ∖ 𝐴 ) = ∅ )
17	10 16	eqtr4d	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → if ( ∅ ∈ 𝐴 , ∅ , 1o ) = ( 1o ∖ 𝐴 ) )
18		on0eqel	⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
19	8 17 18	mpjaodan	⊢ ( 𝐴 ∈ On → if ( ∅ ∈ 𝐴 , ∅ , 1o ) = ( 1o ∖ 𝐴 ) )
20	1 19	eqtr4d	⊢ ( 𝐴 ∈ On → ( ∅ ↑o 𝐴 ) = if ( ∅ ∈ 𝐴 , ∅ , 1o ) )