Metamath Proof Explorer

Theorem oewordi

Description: Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005)

Ref Expression
Assertion oewordi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B

Proof

Step Hyp Ref Expression
1 eloni ⊢ C ∈ On → Ord ⁡ C
2 ordgt0ge1 ⊢ Ord ⁡ C → ∅ ∈ C ↔ 1 𝑜 ⊆ C
3 1 2 syl ⊢ C ∈ On → ∅ ∈ C ↔ 1 𝑜 ⊆ C
4 1on ⊢ 1 𝑜 ∈ On
5 onsseleq ⊢ 1 𝑜 ∈ On ∧ C ∈ On → 1 𝑜 ⊆ C ↔ 1 𝑜 ∈ C ∨ 1 𝑜 = C
6 4 5 mpan ⊢ C ∈ On → 1 𝑜 ⊆ C ↔ 1 𝑜 ∈ C ∨ 1 𝑜 = C
7 3 6 bitrd ⊢ C ∈ On → ∅ ∈ C ↔ 1 𝑜 ∈ C ∨ 1 𝑜 = C
8 7 3ad2ant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∅ ∈ C ↔ 1 𝑜 ∈ C ∨ 1 𝑜 = C
9 ondif2 ⊢ C ∈ On ∖ 2 𝑜 ↔ C ∈ On ∧ 1 𝑜 ∈ C
10 oeword ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ⊆ B ↔ C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
11 10 biimpd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∖ 2 𝑜 → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
12 11 3expia ⊢ A ∈ On ∧ B ∈ On → C ∈ On ∖ 2 𝑜 → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
13 9 12 syl5bir ⊢ A ∈ On ∧ B ∈ On → C ∈ On ∧ 1 𝑜 ∈ C → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
14 13 expd ⊢ A ∈ On ∧ B ∈ On → C ∈ On → 1 𝑜 ∈ C → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
15 14 3impia ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → 1 𝑜 ∈ C → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
16 oe1m ⊢ A ∈ On → 1 𝑜 ↑ 𝑜 A = 1 𝑜
17 16 adantr ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 ↑ 𝑜 A = 1 𝑜
18 oe1m ⊢ B ∈ On → 1 𝑜 ↑ 𝑜 B = 1 𝑜
19 18 adantl ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 ↑ 𝑜 B = 1 𝑜
20 17 19 eqtr4d ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 ↑ 𝑜 A = 1 𝑜 ↑ 𝑜 B
21 eqimss ⊢ 1 𝑜 ↑ 𝑜 A = 1 𝑜 ↑ 𝑜 B → 1 𝑜 ↑ 𝑜 A ⊆ 1 𝑜 ↑ 𝑜 B
22 20 21 syl ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 ↑ 𝑜 A ⊆ 1 𝑜 ↑ 𝑜 B
23 oveq1 ⊢ 1 𝑜 = C → 1 𝑜 ↑ 𝑜 A = C ↑ 𝑜 A
24 oveq1 ⊢ 1 𝑜 = C → 1 𝑜 ↑ 𝑜 B = C ↑ 𝑜 B
25 23 24 sseq12d ⊢ 1 𝑜 = C → 1 𝑜 ↑ 𝑜 A ⊆ 1 𝑜 ↑ 𝑜 B ↔ C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
26 22 25 syl5ibcom ⊢ A ∈ On ∧ B ∈ On → 1 𝑜 = C → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
27 26 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → 1 𝑜 = C → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
28 27 a1dd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → 1 𝑜 = C → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
29 15 28 jaod ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → 1 𝑜 ∈ C ∨ 1 𝑜 = C → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
30 8 29 sylbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∅ ∈ C → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B
31 30 imp ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ⊆ B → C ↑ 𝑜 A ⊆ C ↑ 𝑜 B