Metamath Proof Explorer

Theorem oeordsuc

Description: Ordering property of ordinal exponentiation with a successor exponent. Corollary 8.36 of TakeutiZaring p. 68. (Contributed by NM, 7-Jan-2005)

Ref Expression
Assertion oeordsuc ⊢ B ∈ On ∧ C ∈ On → A ∈ B → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C

Proof

Step Hyp Ref Expression
1 onelon ⊢ B ∈ On ∧ A ∈ B → A ∈ On
2 1 ex ⊢ B ∈ On → A ∈ B → A ∈ On
3 2 adantr ⊢ B ∈ On ∧ C ∈ On → A ∈ B → A ∈ On
4 oewordri ⊢ B ∈ On ∧ C ∈ On → A ∈ B → A ↑ 𝑜 C ⊆ B ↑ 𝑜 C
5 4 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → A ↑ 𝑜 C ⊆ B ↑ 𝑜 C
6 oecl ⊢ A ∈ On ∧ C ∈ On → A ↑ 𝑜 C ∈ On
7 6 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 C ∈ On
8 oecl ⊢ B ∈ On ∧ C ∈ On → B ↑ 𝑜 C ∈ On
9 8 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ↑ 𝑜 C ∈ On
10 simp1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ On
11 omwordri ⊢ A ↑ 𝑜 C ∈ On ∧ B ↑ 𝑜 C ∈ On ∧ A ∈ On → A ↑ 𝑜 C ⊆ B ↑ 𝑜 C → A ↑ 𝑜 C ⋅ 𝑜 A ⊆ B ↑ 𝑜 C ⋅ 𝑜 A
12 7 9 10 11 syl3anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 C ⊆ B ↑ 𝑜 C → A ↑ 𝑜 C ⋅ 𝑜 A ⊆ B ↑ 𝑜 C ⋅ 𝑜 A
13 5 12 syld ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → A ↑ 𝑜 C ⋅ 𝑜 A ⊆ B ↑ 𝑜 C ⋅ 𝑜 A
14 oesuc ⊢ A ∈ On ∧ C ∈ On → A ↑ 𝑜 suc ⁡ C = A ↑ 𝑜 C ⋅ 𝑜 A
15 14 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 suc ⁡ C = A ↑ 𝑜 C ⋅ 𝑜 A
16 15 sseq1d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 suc ⁡ C ⊆ B ↑ 𝑜 C ⋅ 𝑜 A ↔ A ↑ 𝑜 C ⋅ 𝑜 A ⊆ B ↑ 𝑜 C ⋅ 𝑜 A
17 13 16 sylibrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → A ↑ 𝑜 suc ⁡ C ⊆ B ↑ 𝑜 C ⋅ 𝑜 A
18 ne0i ⊢ A ∈ B → B ≠ ∅
19 on0eln0 ⊢ B ∈ On → ∅ ∈ B ↔ B ≠ ∅
20 18 19 syl5ibr ⊢ B ∈ On → A ∈ B → ∅ ∈ B
21 20 adantr ⊢ B ∈ On ∧ C ∈ On → A ∈ B → ∅ ∈ B
22 oen0 ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ B → ∅ ∈ B ↑ 𝑜 C
23 22 ex ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B → ∅ ∈ B ↑ 𝑜 C
24 21 23 syld ⊢ B ∈ On ∧ C ∈ On → A ∈ B → ∅ ∈ B ↑ 𝑜 C
25 omordi ⊢ B ∈ On ∧ B ↑ 𝑜 C ∈ On ∧ ∅ ∈ B ↑ 𝑜 C → A ∈ B → B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 C ⋅ 𝑜 B
26 8 25 syldanl ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ B ↑ 𝑜 C → A ∈ B → B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 C ⋅ 𝑜 B
27 26 ex ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ B ↑ 𝑜 C → A ∈ B → B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 C ⋅ 𝑜 B
28 27 com23 ⊢ B ∈ On ∧ C ∈ On → A ∈ B → ∅ ∈ B ↑ 𝑜 C → B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 C ⋅ 𝑜 B
29 24 28 mpdd ⊢ B ∈ On ∧ C ∈ On → A ∈ B → B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 C ⋅ 𝑜 B
30 29 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 C ⋅ 𝑜 B
31 oesuc ⊢ B ∈ On ∧ C ∈ On → B ↑ 𝑜 suc ⁡ C = B ↑ 𝑜 C ⋅ 𝑜 B
32 31 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ↑ 𝑜 suc ⁡ C = B ↑ 𝑜 C ⋅ 𝑜 B
33 32 eleq2d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 suc ⁡ C ↔ B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 C ⋅ 𝑜 B
34 30 33 sylibrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 suc ⁡ C
35 17 34 jcad ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → A ↑ 𝑜 suc ⁡ C ⊆ B ↑ 𝑜 C ⋅ 𝑜 A ∧ B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 suc ⁡ C
36 35 3expa ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → A ↑ 𝑜 suc ⁡ C ⊆ B ↑ 𝑜 C ⋅ 𝑜 A ∧ B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 suc ⁡ C
37 sucelon ⊢ C ∈ On ↔ suc ⁡ C ∈ On
38 oecl ⊢ A ∈ On ∧ suc ⁡ C ∈ On → A ↑ 𝑜 suc ⁡ C ∈ On
39 oecl ⊢ B ∈ On ∧ suc ⁡ C ∈ On → B ↑ 𝑜 suc ⁡ C ∈ On
40 ontr2 ⊢ A ↑ 𝑜 suc ⁡ C ∈ On ∧ B ↑ 𝑜 suc ⁡ C ∈ On → A ↑ 𝑜 suc ⁡ C ⊆ B ↑ 𝑜 C ⋅ 𝑜 A ∧ B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 suc ⁡ C → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C
41 38 39 40 syl2an ⊢ A ∈ On ∧ suc ⁡ C ∈ On ∧ B ∈ On ∧ suc ⁡ C ∈ On → A ↑ 𝑜 suc ⁡ C ⊆ B ↑ 𝑜 C ⋅ 𝑜 A ∧ B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 suc ⁡ C → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C
42 41 anandirs ⊢ A ∈ On ∧ B ∈ On ∧ suc ⁡ C ∈ On → A ↑ 𝑜 suc ⁡ C ⊆ B ↑ 𝑜 C ⋅ 𝑜 A ∧ B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 suc ⁡ C → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C
43 37 42 sylan2b ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 suc ⁡ C ⊆ B ↑ 𝑜 C ⋅ 𝑜 A ∧ B ↑ 𝑜 C ⋅ 𝑜 A ∈ B ↑ 𝑜 suc ⁡ C → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C
44 36 43 syld ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C
45 44 exp31 ⊢ A ∈ On → B ∈ On → C ∈ On → A ∈ B → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C
46 45 com4l ⊢ B ∈ On → C ∈ On → A ∈ B → A ∈ On → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C
47 46 imp ⊢ B ∈ On ∧ C ∈ On → A ∈ B → A ∈ On → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C
48 3 47 mpdd ⊢ B ∈ On ∧ C ∈ On → A ∈ B → A ↑ 𝑜 suc ⁡ C ∈ B ↑ 𝑜 suc ⁡ C