Metamath Proof Explorer

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 ⊢ A ∈ On ∧ B ∈ On ∧ B ≠ ∅ → A ⊆ A ↑ 𝑜 B

Proof

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