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