Theorem oe0m1

Description: Ordinal exponentiation with zero mantissa and nonzero exponent. Proposition 8.31(2) of TakeutiZaring p. 67 and its converse. (Contributed by NM, 5-Jan-2005)

	Ref	Expression
Assertion	oe0m1	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ ( ∅ ↑o 𝐴 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
2		ordgt0ge1	⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴 ) )
4		oe0m	⊢ ( 𝐴 ∈ On → ( ∅ ↑o 𝐴 ) = ( 1o ∖ 𝐴 ) )
5	4	eqeq1d	⊢ ( 𝐴 ∈ On → ( ( ∅ ↑o 𝐴 ) = ∅ ↔ ( 1o ∖ 𝐴 ) = ∅ ) )
6		ssdif0	⊢ ( 1o ⊆ 𝐴 ↔ ( 1o ∖ 𝐴 ) = ∅ )
7	5 6	syl6rbbr	⊢ ( 𝐴 ∈ On → ( 1o ⊆ 𝐴 ↔ ( ∅ ↑o 𝐴 ) = ∅ ) )
8	3 7	bitrd	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ ( ∅ ↑o 𝐴 ) = ∅ ) )