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 e. On /\ B e. On /\ B =/= (/) ) -> A C_ ( A ^o B ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = (/) -> A = (/) )
2 0ss 
 |-  (/) C_ ( A ^o B )
3 1 2 eqsstrdi 
 |-  ( A = (/) -> A C_ ( A ^o B ) )
4 3 a1i 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> ( A = (/) -> A C_ ( A ^o B ) ) )
5 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ B =/= (/) ) /\ (/) e. A ) -> A e. On )
6 oe1 
 |-  ( A e. On -> ( A ^o 1o ) = A )
7 5 6 syl 
 |-  ( ( ( A e. On /\ B e. On /\ B =/= (/) ) /\ (/) e. A ) -> ( A ^o 1o ) = A )
8 1on 
 |-  1o e. On
9 8 a1i 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> 1o e. On )
10 simp2 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> B e. On )
11 simp1 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> A e. On )
12 9 10 11 3jca 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> ( 1o e. On /\ B e. On /\ A e. On ) )
13 12 anim1i 
 |-  ( ( ( A e. On /\ B e. On /\ B =/= (/) ) /\ (/) e. A ) -> ( ( 1o e. On /\ B e. On /\ A e. On ) /\ (/) e. A ) )
14 eloni 
 |-  ( B e. On -> Ord B )
15 10 14 syl 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> Ord B )
16 simp3 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> B =/= (/) )
17 ordge1n0 
 |-  ( Ord B -> ( 1o C_ B <-> B =/= (/) ) )
18 17 biimprd 
 |-  ( Ord B -> ( B =/= (/) -> 1o C_ B ) )
19 15 16 18 sylc 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> 1o C_ B )
20 19 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ B =/= (/) ) /\ (/) e. A ) -> 1o C_ B )
21 oewordi 
 |-  ( ( ( 1o e. On /\ B e. On /\ A e. On ) /\ (/) e. A ) -> ( 1o C_ B -> ( A ^o 1o ) C_ ( A ^o B ) ) )
22 13 20 21 sylc 
 |-  ( ( ( A e. On /\ B e. On /\ B =/= (/) ) /\ (/) e. A ) -> ( A ^o 1o ) C_ ( A ^o B ) )
23 7 22 eqsstrrd 
 |-  ( ( ( A e. On /\ B e. On /\ B =/= (/) ) /\ (/) e. A ) -> A C_ ( A ^o B ) )
24 23 ex 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> ( (/) e. A -> A C_ ( A ^o B ) ) )
25 on0eqel 
 |-  ( A e. On -> ( A = (/) \/ (/) e. A ) )
26 11 25 syl 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> ( A = (/) \/ (/) e. A ) )
27 4 24 26 mpjaod 
 |-  ( ( A e. On /\ B e. On /\ B =/= (/) ) -> A C_ ( A ^o B ) )