Metamath Proof Explorer

Theorem omlimcl

Description: The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of TakeutiZaring p. 64. (Contributed by NM, 25-Dec-2004)

Ref Expression
Assertion omlimcl 
|- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Lim ( A .o B ) )

Proof

Step Hyp Ref Expression
1 limelon 
 |-  ( ( B e. C /\ Lim B ) -> B e. On )
2 omcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
3 eloni 
 |-  ( ( A .o B ) e. On -> Ord ( A .o B ) )
4 2 3 syl 
 |-  ( ( A e. On /\ B e. On ) -> Ord ( A .o B ) )
5 1 4 sylan2 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> Ord ( A .o B ) )
6 5 adantr 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Ord ( A .o B ) )
7 0ellim 
 |-  ( Lim B -> (/) e. B )
8 n0i 
 |-  ( (/) e. B -> -. B = (/) )
9 7 8 syl 
 |-  ( Lim B -> -. B = (/) )
10 n0i 
 |-  ( (/) e. A -> -. A = (/) )
11 9 10 anim12ci 
 |-  ( ( Lim B /\ (/) e. A ) -> ( -. A = (/) /\ -. B = (/) ) )
12 11 adantll 
 |-  ( ( ( B e. C /\ Lim B ) /\ (/) e. A ) -> ( -. A = (/) /\ -. B = (/) ) )
13 12 adantll 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( -. A = (/) /\ -. B = (/) ) )
14 om00 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )
15 14 notbid 
 |-  ( ( A e. On /\ B e. On ) -> ( -. ( A .o B ) = (/) <-> -. ( A = (/) \/ B = (/) ) ) )
16 ioran 
 |-  ( -. ( A = (/) \/ B = (/) ) <-> ( -. A = (/) /\ -. B = (/) ) )
17 15 16 bitrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( -. ( A .o B ) = (/) <-> ( -. A = (/) /\ -. B = (/) ) ) )
18 1 17 sylan2 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( -. ( A .o B ) = (/) <-> ( -. A = (/) /\ -. B = (/) ) ) )
19 18 adantr 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( -. ( A .o B ) = (/) <-> ( -. A = (/) /\ -. B = (/) ) ) )
20 13 19 mpbird 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> -. ( A .o B ) = (/) )
21 vex 
 |-  y e. _V
22 21 sucid 
 |-  y e. suc y
23 omlim 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A .o B ) = U_ x e. B ( A .o x ) )
24 eqeq1 
 |-  ( ( A .o B ) = suc y -> ( ( A .o B ) = U_ x e. B ( A .o x ) <-> suc y = U_ x e. B ( A .o x ) ) )
25 24 biimpac 
 |-  ( ( ( A .o B ) = U_ x e. B ( A .o x ) /\ ( A .o B ) = suc y ) -> suc y = U_ x e. B ( A .o x ) )
26 23 25 sylan 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ ( A .o B ) = suc y ) -> suc y = U_ x e. B ( A .o x ) )
27 22 26 eleqtrid 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ ( A .o B ) = suc y ) -> y e. U_ x e. B ( A .o x ) )
28 eliun 
 |-  ( y e. U_ x e. B ( A .o x ) <-> E. x e. B y e. ( A .o x ) )
29 27 28 sylib 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ ( A .o B ) = suc y ) -> E. x e. B y e. ( A .o x ) )
30 29 adantlr 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ ( A .o B ) = suc y ) -> E. x e. B y e. ( A .o x ) )
31 onelon 
 |-  ( ( B e. On /\ x e. B ) -> x e. On )
32 1 31 sylan 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> x e. On )
33 onnbtwn 
 |-  ( x e. On -> -. ( x e. B /\ B e. suc x ) )
34 imnan 
 |-  ( ( x e. B -> -. B e. suc x ) <-> -. ( x e. B /\ B e. suc x ) )
35 33 34 sylibr 
 |-  ( x e. On -> ( x e. B -> -. B e. suc x ) )
36 35 com12 
 |-  ( x e. B -> ( x e. On -> -. B e. suc x ) )
37 36 adantl 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> ( x e. On -> -. B e. suc x ) )
38 32 37 mpd 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> -. B e. suc x )
39 38 ad5ant24 
 |-  ( ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ x e. B ) /\ y e. ( A .o x ) ) -> -. B e. suc x )
40 simpl 
 |-  ( ( B e. On /\ x e. B ) -> B e. On )
41 40 31 jca 
 |-  ( ( B e. On /\ x e. B ) -> ( B e. On /\ x e. On ) )
42 1 41 sylan 
 |-  ( ( ( B e. C /\ Lim B ) /\ x e. B ) -> ( B e. On /\ x e. On ) )
43 42 anim2i 
 |-  ( ( A e. On /\ ( ( B e. C /\ Lim B ) /\ x e. B ) ) -> ( A e. On /\ ( B e. On /\ x e. On ) ) )
44 43 anassrs 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ x e. B ) -> ( A e. On /\ ( B e. On /\ x e. On ) ) )
45 omcl 
 |-  ( ( A e. On /\ x e. On ) -> ( A .o x ) e. On )
46 eloni 
 |-  ( ( A .o x ) e. On -> Ord ( A .o x ) )
47 ordsucelsuc 
 |-  ( Ord ( A .o x ) -> ( y e. ( A .o x ) <-> suc y e. suc ( A .o x ) ) )
48 46 47 syl 
 |-  ( ( A .o x ) e. On -> ( y e. ( A .o x ) <-> suc y e. suc ( A .o x ) ) )
49 oa1suc 
 |-  ( ( A .o x ) e. On -> ( ( A .o x ) +o 1o ) = suc ( A .o x ) )
50 49 eleq2d 
 |-  ( ( A .o x ) e. On -> ( suc y e. ( ( A .o x ) +o 1o ) <-> suc y e. suc ( A .o x ) ) )
51 48 50 bitr4d 
 |-  ( ( A .o x ) e. On -> ( y e. ( A .o x ) <-> suc y e. ( ( A .o x ) +o 1o ) ) )
52 45 51 syl 
 |-  ( ( A e. On /\ x e. On ) -> ( y e. ( A .o x ) <-> suc y e. ( ( A .o x ) +o 1o ) ) )
53 52 adantr 
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( y e. ( A .o x ) <-> suc y e. ( ( A .o x ) +o 1o ) ) )
54 eloni 
 |-  ( A e. On -> Ord A )
55 ordgt0ge1 
 |-  ( Ord A -> ( (/) e. A <-> 1o C_ A ) )
56 54 55 syl 
 |-  ( A e. On -> ( (/) e. A <-> 1o C_ A ) )
57 56 adantr 
 |-  ( ( A e. On /\ x e. On ) -> ( (/) e. A <-> 1o C_ A ) )
58 1on 
 |-  1o e. On
59 oaword 
 |-  ( ( 1o e. On /\ A e. On /\ ( A .o x ) e. On ) -> ( 1o C_ A <-> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) ) )
60 58 59 mp3an1 
 |-  ( ( A e. On /\ ( A .o x ) e. On ) -> ( 1o C_ A <-> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) ) )
61 45 60 syldan 
 |-  ( ( A e. On /\ x e. On ) -> ( 1o C_ A <-> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) ) )
62 57 61 bitrd 
 |-  ( ( A e. On /\ x e. On ) -> ( (/) e. A <-> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) ) )
63 62 biimpa 
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( ( A .o x ) +o 1o ) C_ ( ( A .o x ) +o A ) )
64 omsuc 
 |-  ( ( A e. On /\ x e. On ) -> ( A .o suc x ) = ( ( A .o x ) +o A ) )
65 64 adantr 
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( A .o suc x ) = ( ( A .o x ) +o A ) )
66 63 65 sseqtrrd 
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( ( A .o x ) +o 1o ) C_ ( A .o suc x ) )
67 66 sseld 
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( suc y e. ( ( A .o x ) +o 1o ) -> suc y e. ( A .o suc x ) ) )
68 53 67 sylbid 
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> suc y e. ( A .o suc x ) ) )
69 eleq1 
 |-  ( ( A .o B ) = suc y -> ( ( A .o B ) e. ( A .o suc x ) <-> suc y e. ( A .o suc x ) ) )
70 69 biimprd 
 |-  ( ( A .o B ) = suc y -> ( suc y e. ( A .o suc x ) -> ( A .o B ) e. ( A .o suc x ) ) )
71 68 70 syl9 
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( ( A .o B ) = suc y -> ( y e. ( A .o x ) -> ( A .o B ) e. ( A .o suc x ) ) ) )
72 71 com23 
 |-  ( ( ( A e. On /\ x e. On ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> ( A .o B ) e. ( A .o suc x ) ) ) )
73 72 adantlrl 
 |-  ( ( ( A e. On /\ ( B e. On /\ x e. On ) ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> ( A .o B ) e. ( A .o suc x ) ) ) )
74 onsucb 
 |-  ( x e. On <-> suc x e. On )
75 omord 
 |-  ( ( B e. On /\ suc x e. On /\ A e. On ) -> ( ( B e. suc x /\ (/) e. A ) <-> ( A .o B ) e. ( A .o suc x ) ) )
76 simpl 
 |-  ( ( B e. suc x /\ (/) e. A ) -> B e. suc x )
77 75 76 biimtrrdi 
 |-  ( ( B e. On /\ suc x e. On /\ A e. On ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
78 74 77 syl3an2b 
 |-  ( ( B e. On /\ x e. On /\ A e. On ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
79 78 3comr 
 |-  ( ( A e. On /\ B e. On /\ x e. On ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
80 79 3expb 
 |-  ( ( A e. On /\ ( B e. On /\ x e. On ) ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
81 80 adantr 
 |-  ( ( ( A e. On /\ ( B e. On /\ x e. On ) ) /\ (/) e. A ) -> ( ( A .o B ) e. ( A .o suc x ) -> B e. suc x ) )
82 73 81 syl6d 
 |-  ( ( ( A e. On /\ ( B e. On /\ x e. On ) ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> B e. suc x ) ) )
83 44 82 sylan 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ x e. B ) /\ (/) e. A ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> B e. suc x ) ) )
84 83 an32s 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ x e. B ) -> ( y e. ( A .o x ) -> ( ( A .o B ) = suc y -> B e. suc x ) ) )
85 84 imp 
 |-  ( ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ x e. B ) /\ y e. ( A .o x ) ) -> ( ( A .o B ) = suc y -> B e. suc x ) )
86 39 85 mtod 
 |-  ( ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ x e. B ) /\ y e. ( A .o x ) ) -> -. ( A .o B ) = suc y )
87 86 rexlimdva2 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( E. x e. B y e. ( A .o x ) -> -. ( A .o B ) = suc y ) )
88 87 adantr 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ ( A .o B ) = suc y ) -> ( E. x e. B y e. ( A .o x ) -> -. ( A .o B ) = suc y ) )
89 30 88 mpd 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ ( A .o B ) = suc y ) -> -. ( A .o B ) = suc y )
90 89 pm2.01da 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> -. ( A .o B ) = suc y )
91 90 adantr 
 |-  ( ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) /\ y e. On ) -> -. ( A .o B ) = suc y )
92 91 nrexdv 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> -. E. y e. On ( A .o B ) = suc y )
93 ioran 
 |-  ( -. ( ( A .o B ) = (/) \/ E. y e. On ( A .o B ) = suc y ) <-> ( -. ( A .o B ) = (/) /\ -. E. y e. On ( A .o B ) = suc y ) )
94 20 92 93 sylanbrc 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> -. ( ( A .o B ) = (/) \/ E. y e. On ( A .o B ) = suc y ) )
95 dflim3 
 |-  ( Lim ( A .o B ) <-> ( Ord ( A .o B ) /\ -. ( ( A .o B ) = (/) \/ E. y e. On ( A .o B ) = suc y ) ) )
96 6 94 95 sylanbrc 
 |-  ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Lim ( A .o B ) )