Metamath Proof Explorer

Theorem oeword

Description: Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005) (Revised by Mario Carneiro, 24-May-2015)

Ref Expression
Assertion oeword ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ⊆ B ↔ C ↑ 𝑜 A ⊆ C ↑ 𝑜 B

Proof

Step Hyp Ref Expression
1 oeord ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ∈ B ↔ C ↑ 𝑜 A ∈ C ↑ 𝑜 B
2 oecan ⊢ C ∈ On ∖ 2 𝑜 ∧ A ∈ On ∧ B ∈ On → C ↑ 𝑜 A = C ↑ 𝑜 B ↔ A = B
3 2 3coml ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A = C ↑ 𝑜 B ↔ A = B
4 3 bicomd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A = B ↔ C ↑ 𝑜 A = C ↑ 𝑜 B
5 1 4 orbi12d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ∈ B ∨ A = B ↔ C ↑ 𝑜 A ∈ C ↑ 𝑜 B ∨ C ↑ 𝑜 A = C ↑ 𝑜 B
6 onsseleq ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ A ∈ B ∨ A = B
7 6 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ⊆ B ↔ A ∈ B ∨ A = B
8 eldifi ⊢ C ∈ On ∖ 2 𝑜 → C ∈ On
9 id ⊢ A ∈ On ∧ B ∈ On → A ∈ On ∧ B ∈ On
10 oecl ⊢ C ∈ On ∧ A ∈ On → C ↑ 𝑜 A ∈ On
11 oecl ⊢ C ∈ On ∧ B ∈ On → C ↑ 𝑜 B ∈ On
12 10 11 anim12dan ⊢ C ∈ On ∧ A ∈ On ∧ B ∈ On → C ↑ 𝑜 A ∈ On ∧ C ↑ 𝑜 B ∈ On
13 onsseleq ⊢ C ↑ 𝑜 A ∈ On ∧ C ↑ 𝑜 B ∈ On → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B ↔ C ↑ 𝑜 A ∈ C ↑ 𝑜 B ∨ C ↑ 𝑜 A = C ↑ 𝑜 B
14 12 13 syl ⊢ C ∈ On ∧ A ∈ On ∧ B ∈ On → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B ↔ C ↑ 𝑜 A ∈ C ↑ 𝑜 B ∨ C ↑ 𝑜 A = C ↑ 𝑜 B
15 8 9 14 syl2anr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B ↔ C ↑ 𝑜 A ∈ C ↑ 𝑜 B ∨ C ↑ 𝑜 A = C ↑ 𝑜 B
16 15 3impa ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B ↔ C ↑ 𝑜 A ∈ C ↑ 𝑜 B ∨ C ↑ 𝑜 A = C ↑ 𝑜 B
17 5 7 16 3bitr4d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ⊆ B ↔ C ↑ 𝑜 A ⊆ C ↑ 𝑜 B