Metamath Proof Explorer

Theorem omordi

Description: Ordering property of ordinal multiplication. Half of Proposition 8.19 of TakeutiZaring p. 63. (Contributed by NM, 14-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 onelon ⊢ B ∈ On ∧ A ∈ B → A ∈ On
2 1 ex ⊢ B ∈ On → A ∈ B → A ∈ On
3 eleq2 ⊢ x = ∅ → A ∈ x ↔ A ∈ ∅
4 oveq2 ⊢ x = ∅ → C ⋅ 𝑜 x = C ⋅ 𝑜 ∅
5 4 eleq2d ⊢ x = ∅ → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 ∅
6 3 5 imbi12d ⊢ x = ∅ → A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x ↔ A ∈ ∅ → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 ∅
7 eleq2 ⊢ x = y → A ∈ x ↔ A ∈ y
8 oveq2 ⊢ x = y → C ⋅ 𝑜 x = C ⋅ 𝑜 y
9 8 eleq2d ⊢ x = y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y
10 7 9 imbi12d ⊢ x = y → A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x ↔ A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y
11 eleq2 ⊢ x = suc ⁡ y → A ∈ x ↔ A ∈ suc ⁡ y
12 oveq2 ⊢ x = suc ⁡ y → C ⋅ 𝑜 x = C ⋅ 𝑜 suc ⁡ y
13 12 eleq2d ⊢ x = suc ⁡ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ y
14 11 13 imbi12d ⊢ x = suc ⁡ y → A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x ↔ A ∈ suc ⁡ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ y
15 eleq2 ⊢ x = B → A ∈ x ↔ A ∈ B
16 oveq2 ⊢ x = B → C ⋅ 𝑜 x = C ⋅ 𝑜 B
17 16 eleq2d ⊢ x = B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
18 15 17 imbi12d ⊢ x = B → A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x ↔ A ∈ B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
19 noel ⊢ ¬ A ∈ ∅
20 19 pm2.21i ⊢ A ∈ ∅ → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 ∅
21 20 a1i ⊢ A ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ ∅ → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 ∅
22 elsuci ⊢ A ∈ suc ⁡ y → A ∈ y ∨ A = y
23 omcl ⊢ C ∈ On ∧ y ∈ On → C ⋅ 𝑜 y ∈ On
24 simpl ⊢ C ∈ On ∧ y ∈ On → C ∈ On
25 23 24 jca ⊢ C ∈ On ∧ y ∈ On → C ⋅ 𝑜 y ∈ On ∧ C ∈ On
26 oaword1 ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On → C ⋅ 𝑜 y ⊆ C ⋅ 𝑜 y + 𝑜 C
27 26 sseld ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
28 27 imim2d ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On → A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
29 28 imp ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On ∧ A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
30 29 adantrl ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On ∧ ∅ ∈ C ∧ A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
31 oaord1 ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On → ∅ ∈ C ↔ C ⋅ 𝑜 y ∈ C ⋅ 𝑜 y + 𝑜 C
32 31 biimpa ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 y ∈ C ⋅ 𝑜 y + 𝑜 C
33 oveq2 ⊢ A = y → C ⋅ 𝑜 A = C ⋅ 𝑜 y
34 33 eleq1d ⊢ A = y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C ↔ C ⋅ 𝑜 y ∈ C ⋅ 𝑜 y + 𝑜 C
35 32 34 syl5ibrcom ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A = y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
36 35 adantrr ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On ∧ ∅ ∈ C ∧ A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A = y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
37 30 36 jaod ⊢ C ⋅ 𝑜 y ∈ On ∧ C ∈ On ∧ ∅ ∈ C ∧ A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ y ∨ A = y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
38 25 37 sylan ⊢ C ∈ On ∧ y ∈ On ∧ ∅ ∈ C ∧ A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ y ∨ A = y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
39 22 38 syl5 ⊢ C ∈ On ∧ y ∈ On ∧ ∅ ∈ C ∧ A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ suc ⁡ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
40 omsuc ⊢ C ∈ On ∧ y ∈ On → C ⋅ 𝑜 suc ⁡ y = C ⋅ 𝑜 y + 𝑜 C
41 40 eleq2d ⊢ C ∈ On ∧ y ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ y ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
42 41 adantr ⊢ C ∈ On ∧ y ∈ On ∧ ∅ ∈ C ∧ A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ y ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y + 𝑜 C
43 39 42 sylibrd ⊢ C ∈ On ∧ y ∈ On ∧ ∅ ∈ C ∧ A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ suc ⁡ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ y
44 43 exp43 ⊢ C ∈ On → y ∈ On → ∅ ∈ C → A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ suc ⁡ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ y
45 44 com12 ⊢ y ∈ On → C ∈ On → ∅ ∈ C → A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ suc ⁡ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ y
46 45 adantld ⊢ y ∈ On → A ∈ On ∧ C ∈ On → ∅ ∈ C → A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ suc ⁡ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ y
47 46 impd ⊢ y ∈ On → A ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ suc ⁡ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ y
48 id ⊢ C ∈ On ∧ Lim ⁡ x → C ∈ On ∧ Lim ⁡ x
49 48 ad2ant2r ⊢ C ∈ On ∧ A ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ C → C ∈ On ∧ Lim ⁡ x
50 limsuc ⊢ Lim ⁡ x → A ∈ x ↔ suc ⁡ A ∈ x
51 50 biimpa ⊢ Lim ⁡ x ∧ A ∈ x → suc ⁡ A ∈ x
52 oveq2 ⊢ y = suc ⁡ A → C ⋅ 𝑜 y = C ⋅ 𝑜 suc ⁡ A
53 52 ssiun2s ⊢ suc ⁡ A ∈ x → C ⋅ 𝑜 suc ⁡ A ⊆ ⋃ y ∈ x C ⋅ 𝑜 y
54 51 53 syl ⊢ Lim ⁡ x ∧ A ∈ x → C ⋅ 𝑜 suc ⁡ A ⊆ ⋃ y ∈ x C ⋅ 𝑜 y
55 54 adantll ⊢ C ∈ On ∧ Lim ⁡ x ∧ A ∈ x → C ⋅ 𝑜 suc ⁡ A ⊆ ⋃ y ∈ x C ⋅ 𝑜 y
56 vex ⊢ x ∈ V
57 omlim ⊢ C ∈ On ∧ x ∈ V ∧ Lim ⁡ x → C ⋅ 𝑜 x = ⋃ y ∈ x C ⋅ 𝑜 y
58 56 57 mpanr1 ⊢ C ∈ On ∧ Lim ⁡ x → C ⋅ 𝑜 x = ⋃ y ∈ x C ⋅ 𝑜 y
59 58 adantr ⊢ C ∈ On ∧ Lim ⁡ x ∧ A ∈ x → C ⋅ 𝑜 x = ⋃ y ∈ x C ⋅ 𝑜 y
60 55 59 sseqtrrd ⊢ C ∈ On ∧ Lim ⁡ x ∧ A ∈ x → C ⋅ 𝑜 suc ⁡ A ⊆ C ⋅ 𝑜 x
61 49 60 sylan ⊢ C ∈ On ∧ A ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ C ∧ A ∈ x → C ⋅ 𝑜 suc ⁡ A ⊆ C ⋅ 𝑜 x
62 omcl ⊢ C ∈ On ∧ A ∈ On → C ⋅ 𝑜 A ∈ On
63 oaord1 ⊢ C ⋅ 𝑜 A ∈ On ∧ C ∈ On → ∅ ∈ C ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 A + 𝑜 C
64 62 63 sylan ⊢ C ∈ On ∧ A ∈ On ∧ C ∈ On → ∅ ∈ C ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 A + 𝑜 C
65 64 anabss1 ⊢ C ∈ On ∧ A ∈ On → ∅ ∈ C ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 A + 𝑜 C
66 65 biimpa ⊢ C ∈ On ∧ A ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 A + 𝑜 C
67 omsuc ⊢ C ∈ On ∧ A ∈ On → C ⋅ 𝑜 suc ⁡ A = C ⋅ 𝑜 A + 𝑜 C
68 67 adantr ⊢ C ∈ On ∧ A ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 suc ⁡ A = C ⋅ 𝑜 A + 𝑜 C
69 66 68 eleqtrrd ⊢ C ∈ On ∧ A ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ A
70 69 adantrl ⊢ C ∈ On ∧ A ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ A
71 70 adantr ⊢ C ∈ On ∧ A ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ C ∧ A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 suc ⁡ A
72 61 71 sseldd ⊢ C ∈ On ∧ A ∈ On ∧ Lim ⁡ x ∧ ∅ ∈ C ∧ A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x
73 72 exp53 ⊢ C ∈ On → A ∈ On → Lim ⁡ x → ∅ ∈ C → A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x
74 73 com13 ⊢ Lim ⁡ x → A ∈ On → C ∈ On → ∅ ∈ C → A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x
75 74 imp4c ⊢ Lim ⁡ x → A ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x
76 75 a1dd ⊢ Lim ⁡ x → A ∈ On ∧ C ∈ On ∧ ∅ ∈ C → ∀ y ∈ x A ∈ y → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 y → A ∈ x → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 x
77 6 10 14 18 21 47 76 tfinds3 ⊢ B ∈ On → A ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
78 77 com23 ⊢ B ∈ On → A ∈ B → A ∈ On ∧ C ∈ On ∧ ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
79 78 exp4a ⊢ B ∈ On → A ∈ B → A ∈ On ∧ C ∈ On → ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
80 79 exp4a ⊢ B ∈ On → A ∈ B → A ∈ On → C ∈ On → ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
81 2 80 mpdd ⊢ B ∈ On → A ∈ B → C ∈ On → ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
82 81 com34 ⊢ B ∈ On → A ∈ B → ∅ ∈ C → C ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
83 82 com24 ⊢ B ∈ On → C ∈ On → ∅ ∈ C → A ∈ B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
84 83 imp31 ⊢ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B