Theorem oege1

Description: Any nonzero ordinal power is greater-than-or-equal to the term on the left. Lemma 3.19 of Schloeder p. 10. See oewordi . (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	oege1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → 𝐴 ⊆ ( 𝐴 ↑o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
2		0ss	⊢ ∅ ⊆ ( 𝐴 ↑o 𝐵 )
3	1 2	eqsstrdi	⊢ ( 𝐴 = ∅ → 𝐴 ⊆ ( 𝐴 ↑o 𝐵 ) )
4	3	a1i	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∅ → 𝐴 ⊆ ( 𝐴 ↑o 𝐵 ) ) )
5		simpl1	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) ∧ ∅ ∈ 𝐴 ) → 𝐴 ∈ On )
6		oe1	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o 1o ) = 𝐴 )
7	5 6	syl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 1o ) = 𝐴 )
8		1on	⊢ 1o ∈ On
9	8	a1i	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → 1o ∈ On )
10		simp2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → 𝐵 ∈ On )
11		simp1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → 𝐴 ∈ On )
12	9 10 11	3jca	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → ( 1o ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) )
13	12	anim1i	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) ∧ ∅ ∈ 𝐴 ) → ( ( 1o ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) )
14		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
15	10 14	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → Ord 𝐵 )
16		simp3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → 𝐵 ≠ ∅ )
17		ordge1n0	⊢ ( Ord 𝐵 → ( 1o ⊆ 𝐵 ↔ 𝐵 ≠ ∅ ) )
18	17	biimprd	⊢ ( Ord 𝐵 → ( 𝐵 ≠ ∅ → 1o ⊆ 𝐵 ) )
19	15 16 18	sylc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → 1o ⊆ 𝐵 )
20	19	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) ∧ ∅ ∈ 𝐴 ) → 1o ⊆ 𝐵 )
21		oewordi	⊢ ( ( ( 1o ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 1o ⊆ 𝐵 → ( 𝐴 ↑o 1o ) ⊆ ( 𝐴 ↑o 𝐵 ) ) )
22	13 20 21	sylc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 1o ) ⊆ ( 𝐴 ↑o 𝐵 ) )
23	7 22	eqsstrrd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) ∧ ∅ ∈ 𝐴 ) → 𝐴 ⊆ ( 𝐴 ↑o 𝐵 ) )
24	23	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → ( ∅ ∈ 𝐴 → 𝐴 ⊆ ( 𝐴 ↑o 𝐵 ) ) )
25		on0eqel	⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
26	11 25	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
27	4 24 26	mpjaod	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ) → 𝐴 ⊆ ( 𝐴 ↑o 𝐵 ) )