Metamath Proof Explorer

Theorem oaword

Description: Weak ordering property of ordinal addition. (Contributed by NM, 6-Dec-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion oaword ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B ↔ C + 𝑜 A ⊆ C + 𝑜 B

Proof

Step Hyp Ref Expression
1 oaord ⊢ B ∈ On ∧ A ∈ On ∧ C ∈ On → B ∈ A ↔ C + 𝑜 B ∈ C + 𝑜 A
2 1 3com12 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ∈ A ↔ C + 𝑜 B ∈ C + 𝑜 A
3 2 notbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ¬ B ∈ A ↔ ¬ C + 𝑜 B ∈ C + 𝑜 A
4 ontri1 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ¬ B ∈ A
5 4 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B ↔ ¬ B ∈ A
6 oacl ⊢ C ∈ On ∧ A ∈ On → C + 𝑜 A ∈ On
7 6 ancoms ⊢ A ∈ On ∧ C ∈ On → C + 𝑜 A ∈ On
8 7 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C + 𝑜 A ∈ On
9 oacl ⊢ C ∈ On ∧ B ∈ On → C + 𝑜 B ∈ On
10 9 ancoms ⊢ B ∈ On ∧ C ∈ On → C + 𝑜 B ∈ On
11 10 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C + 𝑜 B ∈ On
12 ontri1 ⊢ C + 𝑜 A ∈ On ∧ C + 𝑜 B ∈ On → C + 𝑜 A ⊆ C + 𝑜 B ↔ ¬ C + 𝑜 B ∈ C + 𝑜 A
13 8 11 12 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C + 𝑜 A ⊆ C + 𝑜 B ↔ ¬ C + 𝑜 B ∈ C + 𝑜 A
14 3 5 13 3bitr4d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ B ↔ C + 𝑜 A ⊆ C + 𝑜 B