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