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 ( ( ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) ∧ 𝐵 ∈ On ) → 𝐵 ⊆ ( 𝐴 ↑o 𝐵 ) )

Proof

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