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 e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )

Proof

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