Metamath Proof Explorer

Theorem omord2

Description: Ordering property of ordinal multiplication. (Contributed by NM, 25-Dec-2004)

Ref Expression
Assertion omord2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B

Proof

Step Hyp Ref Expression
1 omordi ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
2 1 3adantl1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
3 oveq2 ⊢ A = B → C ⋅ 𝑜 A = C ⋅ 𝑜 B
4 3 a1i ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A = B → C ⋅ 𝑜 A = C ⋅ 𝑜 B
5 omordi ⊢ A ∈ On ∧ C ∈ On ∧ ∅ ∈ C → B ∈ A → C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
6 5 3adantl2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → B ∈ A → C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
7 4 6 orim12d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A = B ∨ B ∈ A → C ⋅ 𝑜 A = C ⋅ 𝑜 B ∨ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
8 7 con3d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → ¬ C ⋅ 𝑜 A = C ⋅ 𝑜 B ∨ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A → ¬ A = B ∨ B ∈ A
9 omcl ⊢ C ∈ On ∧ A ∈ On → C ⋅ 𝑜 A ∈ On
10 omcl ⊢ C ∈ On ∧ B ∈ On → C ⋅ 𝑜 B ∈ On
11 eloni ⊢ C ⋅ 𝑜 A ∈ On → Ord ⁡ C ⋅ 𝑜 A
12 eloni ⊢ C ⋅ 𝑜 B ∈ On → Ord ⁡ C ⋅ 𝑜 B
13 ordtri2 ⊢ Ord ⁡ C ⋅ 𝑜 A ∧ Ord ⁡ C ⋅ 𝑜 B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ↔ ¬ C ⋅ 𝑜 A = C ⋅ 𝑜 B ∨ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
14 11 12 13 syl2an ⊢ C ⋅ 𝑜 A ∈ On ∧ C ⋅ 𝑜 B ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ↔ ¬ C ⋅ 𝑜 A = C ⋅ 𝑜 B ∨ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
15 9 10 14 syl2an ⊢ C ∈ On ∧ A ∈ On ∧ C ∈ On ∧ B ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ↔ ¬ C ⋅ 𝑜 A = C ⋅ 𝑜 B ∨ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
16 15 anandis ⊢ C ∈ On ∧ A ∈ On ∧ B ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ↔ ¬ C ⋅ 𝑜 A = C ⋅ 𝑜 B ∨ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
17 16 ancoms ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ↔ ¬ C ⋅ 𝑜 A = C ⋅ 𝑜 B ∨ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
18 17 3impa ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ↔ ¬ C ⋅ 𝑜 A = C ⋅ 𝑜 B ∨ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
19 18 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ↔ ¬ C ⋅ 𝑜 A = C ⋅ 𝑜 B ∨ C ⋅ 𝑜 B ∈ C ⋅ 𝑜 A
20 eloni ⊢ A ∈ On → Ord ⁡ A
21 eloni ⊢ B ∈ On → Ord ⁡ B
22 ordtri2 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ↔ ¬ A = B ∨ B ∈ A
23 20 21 22 syl2an ⊢ A ∈ On ∧ B ∈ On → A ∈ B ↔ ¬ A = B ∨ B ∈ A
24 23 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ↔ ¬ A = B ∨ B ∈ A
25 24 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B ↔ ¬ A = B ∨ B ∈ A
26 8 19 25 3imtr4d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B → A ∈ B
27 2 26 impbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B