Metamath Proof Explorer

Theorem omordi

Description: Ordering property of ordinal multiplication. Half of Proposition 8.19 of TakeutiZaring p. 63. Lemma 3.15 of Schloeder p. 9. (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∈xC⋅𝑜y
54 51 53 syl ⊢Lim⁡x∧A∈x→C⋅𝑜suc⁡A⊆⋃y∈xC⋅𝑜y
55 54 adantll ⊢C∈On∧Lim⁡x∧A∈x→C⋅𝑜suc⁡A⊆⋃y∈xC⋅𝑜y
56 vex ⊢x∈V
57 omlim ⊢C∈On∧x∈V∧Lim⁡x→C⋅𝑜x=⋃y∈xC⋅𝑜y
58 56 57 mpanr1 ⊢C∈On∧Lim⁡x→C⋅𝑜x=⋃y∈xC⋅𝑜y
59 58 adantr ⊢C∈On∧Lim⁡x∧A∈x→C⋅𝑜x=⋃y∈xC⋅𝑜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∈xA∈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