Metamath Proof Explorer

Theorem oege1

Description: Any non-zero 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