Metamath Proof Explorer

Theorem oege2

Description: Any power of an ordinal at least as large as two is greater-than-or-equal to the term on the right. Lemma 3.20 of Schloeder p. 10. See oeworde . (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion oege2 ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → B ⊆ A ↑ 𝑜 B

Proof

Step Hyp Ref Expression
1 2on ⊢ 2 𝑜 ∈ On
2 1oelpr ⊢ 1 𝑜 ∈ ∅ 1 𝑜
3 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
4 2 3 eleqtrri ⊢ 1 𝑜 ∈ 2 𝑜
5 ondif2 ⊢ 2 𝑜 ∈ On ∖ 2 𝑜 ↔ 2 𝑜 ∈ On ∧ 1 𝑜 ∈ 2 𝑜
6 1 4 5 mpbir2an ⊢ 2 𝑜 ∈ On ∖ 2 𝑜
7 oeworde ⊢ 2 𝑜 ∈ On ∖ 2 𝑜 ∧ B ∈ On → B ⊆ 2 𝑜 ↑ 𝑜 B
8 6 7 mpan ⊢ B ∈ On → B ⊆ 2 𝑜 ↑ 𝑜 B
9 8 adantl ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → B ⊆ 2 𝑜 ↑ 𝑜 B
10 df-2o ⊢ 2 𝑜 = suc ⁡ 1 𝑜
11 onsucss ⊢ A ∈ On → 1 𝑜 ∈ A → suc ⁡ 1 𝑜 ⊆ A
12 11 imp ⊢ A ∈ On ∧ 1 𝑜 ∈ A → suc ⁡ 1 𝑜 ⊆ A
13 12 adantr ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → suc ⁡ 1 𝑜 ⊆ A
14 10 13 eqsstrid ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → 2 𝑜 ⊆ A
15 simpll ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → A ∈ On
16 onsseleq ⊢ 2 𝑜 ∈ On ∧ A ∈ On → 2 𝑜 ⊆ A ↔ 2 𝑜 ∈ A ∨ 2 𝑜 = A
17 1 15 16 sylancr ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → 2 𝑜 ⊆ A ↔ 2 𝑜 ∈ A ∨ 2 𝑜 = A
18 oewordri ⊢ A ∈ On ∧ B ∈ On → 2 𝑜 ∈ A → 2 𝑜 ↑ 𝑜 B ⊆ A ↑ 𝑜 B
19 18 adantlr ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → 2 𝑜 ∈ A → 2 𝑜 ↑ 𝑜 B ⊆ A ↑ 𝑜 B
20 oveq1 ⊢ 2 𝑜 = A → 2 𝑜 ↑ 𝑜 B = A ↑ 𝑜 B
21 ssid ⊢ A ↑ 𝑜 B ⊆ A ↑ 𝑜 B
22 20 21 eqsstrdi ⊢ 2 𝑜 = A → 2 𝑜 ↑ 𝑜 B ⊆ A ↑ 𝑜 B
23 22 a1i ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → 2 𝑜 = A → 2 𝑜 ↑ 𝑜 B ⊆ A ↑ 𝑜 B
24 19 23 jaod ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → 2 𝑜 ∈ A ∨ 2 𝑜 = A → 2 𝑜 ↑ 𝑜 B ⊆ A ↑ 𝑜 B
25 17 24 sylbid ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → 2 𝑜 ⊆ A → 2 𝑜 ↑ 𝑜 B ⊆ A ↑ 𝑜 B
26 14 25 mpd ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → 2 𝑜 ↑ 𝑜 B ⊆ A ↑ 𝑜 B
27 9 26 sstrd ⊢ A ∈ On ∧ 1 𝑜 ∈ A ∧ B ∈ On → B ⊆ A ↑ 𝑜 B